:: PRE_TOPC semantic presentation

K96() is set

bool K96() is non empty set

{} is empty set

1 is non empty set

union {} is set

{{}} is non empty set

T is non empty set

{{},T} is non empty set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

y is set

y is Element of bool (bool T)

Q is Element of bool (bool T)

(T,Q) is () ()

the carrier of (T,Q) is set

the of (T,Q) is Element of bool (bool the carrier of (T,Q))

bool the carrier of (T,Q) is non empty set

bool (bool the carrier of (T,Q)) is non empty set

P is Element of bool (bool the carrier of (T,Q))

union P is Element of bool the carrier of (T,Q)

{T} is non empty set

{} \/ T is non empty set

P is Element of bool the carrier of (T,Q)

Q is Element of bool the carrier of (T,Q)

P /\ Q is Element of bool the carrier of (T,Q)

T is non empty set

bool T is non empty set

bool (bool T) is non empty set

c

(T,c

the carrier of (T,c

the of (T,c

bool the carrier of (T,c

bool (bool the carrier of (T,c

T is non empty set

bool T is non empty set

bool (bool T) is non empty set

c

(T,c

the carrier of (T,c

the of (T,c

bool the carrier of (T,c

bool (bool the carrier of (T,c

T is () ()

the of T is Element of bool (bool the carrier of T)

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

T is () ()

the of T is non empty Element of bool (bool the carrier of T)

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

c

T is 1-sorted

the carrier of T is set

bool the carrier of T is non empty set

[#] T is non proper Element of bool the carrier of T

c

c

the carrier of T \ c

c

[#] the carrier of T is non proper Element of bool the carrier of T

T is 1-sorted

the carrier of T is set

bool the carrier of T is non empty set

[#] T is non proper Element of bool the carrier of T

c

([#] T) \ c

([#] T) \ (([#] T) \ c

c

T is 1-sorted

the carrier of T is set

bool the carrier of T is non empty set

[#] T is non proper Element of bool the carrier of T

c

([#] T) \ c

T is 1-sorted

the carrier of T is set

bool the carrier of T is non empty set

[#] T is non proper Element of bool the carrier of T

c

y is Element of bool the carrier of T

c

([#] T) \ c

y \ c

T is 1-sorted

[#] T is non proper Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

{} T is empty Element of bool the carrier of T

({} T) ` is Element of bool the carrier of T

the carrier of T \ ({} T) is set

T is ()

the carrier of T is set

bool the carrier of T is non empty set

T is ()

the carrier of T is set

bool the carrier of T is non empty set

T is ()

[#] T is non proper Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

the of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

c

y is Element of bool the carrier of T

y /\ ([#] T) is Element of bool the carrier of T

y is Element of bool the carrier of T

y /\ ([#] T) is Element of bool the carrier of T

T is ()

the carrier of T is set

the of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

[#] ( the carrier of T, the of T) is non proper Element of bool the carrier of ( the carrier of T, the of T)

the carrier of ( the carrier of T, the of T) is set

bool the carrier of ( the carrier of T, the of T) is non empty set

[#] T is non proper Element of bool the carrier of T

the of ( the carrier of T, the of T) is Element of bool (bool the carrier of ( the carrier of T, the of T))

bool (bool the carrier of ( the carrier of T, the of T)) is non empty set

y is Element of bool the carrier of ( the carrier of T, the of T)

Q is Element of bool the carrier of T

h is Element of bool the carrier of T

h /\ ([#] ( the carrier of T, the of T)) is Element of bool the carrier of ( the carrier of T, the of T)

Q is Element of bool the carrier of T

Q /\ ([#] ( the carrier of T, the of T)) is Element of bool the carrier of ( the carrier of T, the of T)

T is ()

the carrier of T is set

the of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

T is non empty ()

the carrier of T is non empty set

the of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

T is () ()

c

the carrier of c

[#] T is non proper Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

the of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

[#] c

bool the carrier of c

([#] T) /\ the carrier of c

the of c

bool (bool the carrier of c

Q is Element of bool (bool the carrier of c

union Q is Element of bool the carrier of c

h is Element of bool (bool the carrier of T)

union h is Element of bool the carrier of T

(union h) /\ the carrier of c

P is set

Q is set

Q /\ the carrier of c

P is set

P is set

Q is set

Q is Element of bool the carrier of T

Q /\ the carrier of c

Q is Element of bool the carrier of c

h is Element of bool the carrier of c

Q /\ h is Element of bool the carrier of c

P is Element of bool the carrier of T

P /\ the carrier of c

Q is Element of bool the carrier of T

Q /\ the carrier of c

(Q /\ the carrier of c

P /\ ((Q /\ the carrier of c

the carrier of c

Q /\ ( the carrier of c

P /\ (Q /\ ( the carrier of c

P /\ Q is Element of bool the carrier of T

(P /\ Q) /\ the carrier of c

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

the of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

bool c

bool (bool c

y is Element of bool (bool c

Q is Element of bool (bool c

(c

the carrier of (c

bool the carrier of (c

[#] (c

P is Element of bool the carrier of (c

Q is Element of bool the carrier of T

Q /\ c

Q is Element of bool the carrier of T

Q /\ ([#] (c

[#] T is non proper Element of bool the carrier of T

P is () (T)

[#] P is non proper Element of bool the carrier of P

the carrier of P is set

bool the carrier of P is non empty set

y is () (T)

[#] y is non proper Element of bool the carrier of y

the carrier of y is set

bool the carrier of y is non empty set

Q is () (T)

[#] Q is non proper Element of bool the carrier of Q

the carrier of Q is set

bool the carrier of Q is non empty set

the of Q is Element of bool (bool the carrier of Q)

bool (bool the carrier of Q) is non empty set

the of y is Element of bool (bool the carrier of y)

bool (bool the carrier of y) is non empty set

h is set

the of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

P is Element of bool the carrier of T

P /\ ([#] y) is Element of bool the carrier of y

h is set

the of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

P is Element of bool the carrier of T

P /\ ([#] Q) is Element of bool the carrier of Q

T is non empty ()

the carrier of T is non empty set

bool the carrier of T is non empty set

c

(T,c

[#] (T,c

the carrier of (T,c

bool the carrier of (T,c

T is () ()

the () () (T) is () () (T)

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

c

(T,c

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

y is Element of bool the carrier of T

(T,y) is () () (T)

the carrier of (T,y) is set

bool the carrier of (T,y) is non empty set

c

(T,c

Q is Element of bool the carrier of (T,y)

((T,y),Q) is () () ((T,y))

[#] ((T,y),Q) is non proper Element of bool the carrier of ((T,y),Q)

the carrier of ((T,y),Q) is set

bool the carrier of ((T,y),Q) is non empty set

[#] (T,y) is non proper Element of bool the carrier of (T,y)

the of ((T,y),Q) is non empty Element of bool (bool the carrier of ((T,y),Q))

bool (bool the carrier of ((T,y),Q)) is non empty set

the of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

h is Element of bool the carrier of ((T,y),Q)

P is Element of bool the carrier of T

P /\ ([#] ((T,y),Q)) is Element of bool the carrier of ((T,y),Q)

P /\ ([#] (T,y)) is Element of bool the carrier of (T,y)

Q is Element of bool the carrier of (T,y)

the of (T,y) is non empty Element of bool (bool the carrier of (T,y))

bool (bool the carrier of (T,y)) is non empty set

Q /\ ([#] ((T,y),Q)) is Element of bool the carrier of ((T,y),Q)

y /\ c

P /\ (y /\ c

P is Element of bool the carrier of (T,y)

P /\ ([#] ((T,y),Q)) is Element of bool the carrier of ((T,y),Q)

Q is Element of bool the carrier of T

Q /\ ([#] (T,y)) is Element of bool the carrier of (T,y)

Q /\ (y /\ c

Q /\ ([#] ((T,y),Q)) is Element of bool the carrier of ((T,y),Q)

P is Element of bool the carrier of T

P /\ ([#] ((T,y),Q)) is Element of bool the carrier of ((T,y),Q)

Q is Element of bool the carrier of T

Q /\ ([#] ((T,y),Q)) is Element of bool the carrier of ((T,y),Q)

[#] T is non proper Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

(T,c

the carrier of (T,c

[#] (T,c

bool the carrier of (T,c

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

the carrier of c

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

y is V7() V10( the carrier of T) V11( the carrier of c

Q is Element of bool the carrier of T

y | Q is V7() V10( the carrier of T) V11( the carrier of c

(T,Q) is () (T)

the carrier of (T,Q) is set

[: the carrier of (T,Q), the carrier of c

bool [: the carrier of (T,Q), the carrier of c

T is ()

the carrier of T is set

c

the carrier of c

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

T is ()

the carrier of T is set

the of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

c

the carrier of c

the of c

bool the carrier of c

bool (bool the carrier of c

( the carrier of c

y is ()

the carrier of y is set

the of y is Element of bool (bool the carrier of y)

bool the carrier of y is non empty set

bool (bool the carrier of y) is non empty set

( the carrier of y, the of y) is () ()

Q is ()

the carrier of Q is set

the of Q is Element of bool (bool the carrier of Q)

bool the carrier of Q is non empty set

bool (bool the carrier of Q) is non empty set

( the carrier of Q, the of Q) is () ()

[#] y is non proper Element of bool the carrier of y

[#] T is non proper Element of bool the carrier of T

[#] Q is non proper Element of bool the carrier of Q

[#] c

h is Element of bool the carrier of Q

Q is Element of bool the carrier of c

P is Element of bool the carrier of Q

Q /\ ([#] Q) is Element of bool the carrier of Q

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

the carrier of c

bool the carrier of c

y is Element of bool the carrier of c

[#] c

[#] T is non proper Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

{} T is empty Element of bool the carrier of T

c

the Element of c

T is () ()

[#] T is non proper Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

{} T is empty Element of bool the carrier of T

the of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

([#] T) \ ([#] T) is Element of bool the carrier of T

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

[#] T is non proper (T) Element of bool the carrier of T

T is non empty () ()

the carrier of T is non empty set

bool the carrier of T is non empty set

[#] T is non empty non proper (T) Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

the carrier of c

bool the carrier of c

[#] c

y is Element of bool the carrier of c

([#] c

the of c

bool (bool the carrier of c

the of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

Q is Element of bool the carrier of T

Q /\ ([#] c

[#] T is non proper Element of bool the carrier of T

([#] T) \ Q is Element of bool the carrier of T

(([#] T) \ Q) /\ ([#] c

Q ` is Element of bool the carrier of T

the carrier of T \ Q is set

([#] c

([#] c

([#] c

([#] c

([#] T) \ (([#] T) \ Q) is Element of bool the carrier of T

h is Element of bool the carrier of T

Q is Element of bool the carrier of T

Q /\ ([#] c

([#] T) \ Q is Element of bool the carrier of T

(([#] T) \ Q) /\ ([#] c

([#] c

Q ` is Element of bool the carrier of T

the carrier of T \ Q is set

([#] c

Q is Element of bool the carrier of T

Q /\ ([#] c

h is Element of bool the carrier of T

h /\ ([#] c

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

c

meet c

[#] T is non proper (T) Element of bool the carrier of T

y is Element of bool (bool the carrier of T)

Q is set

h is Element of bool the carrier of T

([#] T) \ h is Element of bool the carrier of T

h is Element of bool the carrier of T

([#] T) \ h is Element of bool the carrier of T

([#] T) \ (([#] T) \ h) is Element of bool the carrier of T

union y is Element of bool the carrier of T

([#] T) \ (union y) is Element of bool the carrier of T

Q is set

h is Element of bool the carrier of T

h is set

h is Element of bool the carrier of T

h is set

Q is set

h is Element of bool the carrier of T

([#] T) \ h is Element of bool the carrier of T

([#] T) \ (([#] T) \ h) is Element of bool the carrier of T

the of T is non empty Element of bool (bool the carrier of T)

([#] T) \ (([#] T) \ (union y)) is Element of bool the carrier of T

the of T is non empty Element of bool (bool the carrier of T)

[#] T is non proper (T) Element of bool the carrier of T

{} T is empty Element of bool the carrier of T

([#] T) \ ({} T) is Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

y is Element of bool the carrier of T

Q is set

h is Element of bool the carrier of T

y is Element of bool the carrier of T

Q is Element of bool the carrier of T

h is set

P is Element of bool the carrier of T

P is Element of bool the carrier of T

y is Element of bool the carrier of T

Q is Element of bool the carrier of T

h is set

P is Element of bool the carrier of T

P is Element of bool the carrier of T

[#] T is non proper Element of bool the carrier of T

([#] T) \ P is Element of bool the carrier of T

Q is set

(([#] T) \ P) ` is Element of bool the carrier of T

the carrier of T \ (([#] T) \ P) is set

P is Element of bool the carrier of T

([#] T) \ P is Element of bool the carrier of T

([#] T) \ (([#] T) \ P) is Element of bool the carrier of T

P ` is Element of bool the carrier of T

the carrier of T \ P is set

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

(T,c

y is set

Q is Element of bool the carrier of T

[#] T is non proper Element of bool the carrier of T

([#] T) \ Q is Element of bool the carrier of T

([#] T) \ (([#] T) \ Q) is Element of bool the carrier of T

Q ` is Element of bool the carrier of T

the carrier of T \ Q is set

Q is Element of bool the carrier of T

[#] T is non proper Element of bool the carrier of T

([#] T) \ Q is Element of bool the carrier of T

(([#] T) \ Q) ` is Element of bool the carrier of T

the carrier of T \ (([#] T) \ Q) is set

Q is Element of bool the carrier of T

h is Element of bool the carrier of T

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

c

(T,c

y is Element of bool (bool the carrier of T)

Q is Element of bool (bool the carrier of T)

meet Q is Element of bool the carrier of T

h is Element of bool the carrier of T

P is Element of bool the carrier of T

[#] T is non proper (T) Element of bool the carrier of T

h is set

P is Element of bool the carrier of T

P is set

Q is Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

the carrier of c

bool the carrier of c

[#] c

y is Element of bool the carrier of T

(T,y) is Element of bool the carrier of T

(T,y) /\ ([#] c

Q is Element of bool the carrier of c

(c

h is set

Q is Element of bool the carrier of T

Q /\ ([#] c

P is Element of bool the carrier of T

P is Element of bool the carrier of c

Q is Element of bool the carrier of T

Q /\ ([#] c

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

(T,c

y is set

Q is Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

y is Element of bool the carrier of T

(T,c

(T,y) is Element of bool the carrier of T

Q is set

h is Element of bool the carrier of T

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

c

y is Element of bool the carrier of T

c

(T,(c

(T,c

(T,y) is Element of bool the carrier of T

(T,c

Q is set

h is Element of bool the carrier of T

c

P is Element of bool the carrier of T

the of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

y /\ P is Element of bool the carrier of T

h /\ P is Element of bool the carrier of T

(c

c

P /\ h is Element of bool the carrier of T

y /\ (P /\ h) is Element of bool the carrier of T

(c

(c

((c

{} /\ h is Element of bool the carrier of T

{} \/ ({} /\ h) is set

{} T is empty Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

y is Element of bool the carrier of T

c

(T,(c

(T,c

(T,y) is Element of bool the carrier of T

(T,c

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

(T,c

y is set

bool (bool the carrier of T) is non empty set

y is Element of bool (bool the carrier of T)

meet y is Element of bool the carrier of T

Q is Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

[#] T is non proper Element of bool the carrier of T

c

([#] T) \ c

(T,(([#] T) \ c

([#] T) \ (([#] T) \ c

T is ()

the carrier of T is set

bool the carrier of T is non empty set

h is ()

the carrier of h is set

bool the carrier of h is non empty set

y is Element of the carrier of T

c

(T,c

Q is Element of bool the carrier of T

Q is Element of the carrier of h

P is Element of bool the carrier of h

(h,P) is Element of bool the carrier of h

T is non empty ()

the carrier of T is non empty set

c

the carrier of c

[#] c

bool the carrier of c

[#] T is non empty non proper Element of bool the carrier of T

bool the carrier of T is non empty set

y is Element of the carrier of c

T is () ()

the carrier of T is set

y is () ()

the carrier of y is set

[: the carrier of T, the carrier of y:] is set

bool [: the carrier of T, the carrier of y:] is non empty set

c

the carrier of c

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

Q is V7() V10( the carrier of T) V11( the carrier of y) V12() V21( the carrier of T, the carrier of y) Element of bool [: the carrier of T, the carrier of y:]

h is V7() V10( the carrier of T) V11( the carrier of c

bool the carrier of c

P is Element of bool the carrier of c

h " P is Element of bool the carrier of T

bool the carrier of T is non empty set

rng h is Element of bool the carrier of c

(rng h) /\ P is Element of bool the carrier of c

h " ((rng h) /\ P) is Element of bool the carrier of T

[#] y is non proper (y) Element of bool the carrier of y

bool the carrier of y is non empty set

(rng h) /\ ([#] y) is Element of bool the carrier of y

((rng h) /\ ([#] y)) /\ P is Element of bool the carrier of c

h " (((rng h) /\ ([#] y)) /\ P) is Element of bool the carrier of T

([#] y) /\ P is Element of bool the carrier of c

(rng h) /\ (([#] y) /\ P) is Element of bool the carrier of c

h " ((rng h) /\ (([#] y) /\ P)) is Element of bool the carrier of T

P /\ ([#] y) is Element of bool the carrier of y

h " (P /\ ([#] y)) is Element of bool the carrier of T

Q is () (c

the carrier of Q is set

bool the carrier of Q is non empty set

[#] Q is non proper (Q) Element of bool the carrier of Q

P /\ ([#] Q) is Element of bool the carrier of Q

Q is Element of bool the carrier of Q

T is () ()

the carrier of T is set

c

the carrier of c

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

y is V7() V10( the carrier of T) V11( the carrier of c

Q is () (c

the carrier of Q is set

[: the carrier of T, the carrier of Q:] is set

bool [: the carrier of T, the carrier of Q:] is non empty set

h is V7() V10( the carrier of T) V11( the carrier of Q) V12() V21( the carrier of T, the carrier of Q) Element of bool [: the carrier of T, the carrier of Q:]

rng y is Element of bool the carrier of c

bool the carrier of c

bool the carrier of Q is non empty set

P is Element of bool the carrier of Q

h " P is Element of bool the carrier of T

bool the carrier of T is non empty set

[#] Q is non proper (Q) Element of bool the carrier of Q

Q is Element of bool the carrier of c

Q /\ ([#] Q) is Element of bool the carrier of Q

y " Q is Element of bool the carrier of T

y " ([#] Q) is Element of bool the carrier of T

(y " Q) /\ (y " ([#] Q)) is Element of bool the carrier of T

(rng y) /\ ([#] Q) is Element of bool the carrier of Q

y " ((rng y) /\ ([#] Q)) is Element of bool the carrier of T

(y " Q) /\ (y " ((rng y) /\ ([#] Q))) is Element of bool the carrier of T

y " (rng y) is Element of bool the carrier of T

(y " Q) /\ (y " (rng y)) is Element of bool the carrier of T

dom y is Element of bool the carrier of T

(y " Q) /\ (dom y) is Element of bool the carrier of T

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

c

{} T is empty Element of bool the carrier of T

the of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

[#] T is non proper (T) Element of bool the carrier of T

([#] T) \ c

c

the carrier of c

T is () ()

y is Element of the carrier of c

T --> y is V7() V10( the carrier of T) V11( the carrier of c

the carrier of T is set

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

K119( the carrier of c

bool the carrier of c

Q is Element of bool the carrier of c

(T --> y) " Q is Element of bool the carrier of T

bool the carrier of T is non empty set

[#] T is non proper (T) Element of bool the carrier of T

{} T is empty (T) Element of bool the carrier of T

T is () ()

the carrier of T is set

c

the carrier of c

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

the Element of the carrier of c

T --> the Element of the carrier of c

K119( the carrier of c

T is ()

T is ()

T is ()

T is ()

bool 1 is non empty Element of bool (bool 1)

bool 1 is non empty set

bool (bool 1) is non empty set

[#] (bool 1) is non empty non proper Element of bool (bool 1)

bool (bool 1) is non empty set

(1,([#] (bool 1))) is () ()

the carrier of (1,([#] (bool 1))) is set

[#] the carrier of (1,([#] (bool 1))) is non proper Element of bool the carrier of (1,([#] (bool 1)))

bool the carrier of (1,([#] (bool 1))) is non empty set

bool (bool the carrier of (1,([#] (bool 1)))) is non empty set

the of (1,([#] (bool 1))) is Element of bool (bool the carrier of (1,([#] (bool 1))))

c

union c

c

y is Element of bool the carrier of (1,([#] (bool 1)))

c

c

the carrier of c

y is Element of the carrier of c

Q is Element of the carrier of c

bool the carrier of c

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

y is Element of the carrier of T

Q is Element of bool the carrier of T

Q ` is Element of bool the carrier of T

the carrier of T \ Q is set

T is ()

the carrier of T is set

c

y is Element of the carrier of T

bool the carrier of T is non empty set

Q is Element of bool the carrier of T

h is Element of bool the carrier of T

Q ` is Element of bool the carrier of T

the carrier of T \ Q is set

T is () ()

the carrier of T is set

the of T is non empty Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

the carrier of ( the carrier of T, the of T) is set

the of ( the carrier of T, the of T) is Element of bool (bool the carrier of ( the carrier of T, the of T))

bool the carrier of ( the carrier of T, the of T) is non empty set

bool (bool the carrier of ( the carrier of T, the of T)) is non empty set

y is Element of bool (bool the carrier of ( the carrier of T, the of T))

union y is Element of bool the carrier of ( the carrier of T, the of T)

Q is Element of bool the carrier of ( the carrier of T, the of T)

h is Element of bool the carrier of ( the carrier of T, the of T)

Q /\ h is Element of bool the carrier of ( the carrier of T, the of T)

T is non empty ()

the carrier of T is non empty set

the of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

T is ()

the carrier of T is set

the of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

the carrier of ( the carrier of T, the of T) is set

the of ( the carrier of T, the of T) is Element of bool (bool the carrier of ( the carrier of T, the of T))

bool the carrier of ( the carrier of T, the of T) is non empty set

bool (bool the carrier of ( the carrier of T, the of T)) is non empty set

y is Element of bool (bool the carrier of T)

union y is Element of bool the carrier of T

Q is Element of bool the carrier of T

h is Element of bool the carrier of T

Q /\ h is Element of bool the carrier of T

T is ()

the carrier of T is set

the of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

c

[#] c

the carrier of c

bool the carrier of c

[#] ( the carrier of T, the of T) is non proper Element of bool the carrier of ( the carrier of T, the of T)

the carrier of ( the carrier of T, the of T) is set

bool the carrier of ( the carrier of T, the of T) is non empty set

[#] T is non proper Element of bool the carrier of T

the of c

bool (bool the carrier of c

y is Element of bool the carrier of c

h is Element of bool the carrier of T

Q is Element of bool the carrier of c

h /\ ([#] c

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

{} T is empty (T) Element of bool the carrier of T

the of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

the of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () () ()

the carrier of ( the carrier of T, the of T) is set

bool the carrier of ( the carrier of T, the of T) is non empty set

c

the of ( the carrier of T, the of T) is non empty Element of bool (bool the carrier of ( the carrier of T, the of T))

bool (bool the carrier of ( the carrier of T, the of T)) is non empty set

T is () ()

the carrier of T is set

bool the carrier of T is non empty set

the of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () () ()

the carrier of ( the carrier of T, the of T) is set

bool the carrier of ( the carrier of T, the of T) is non empty set

c

[#] T is non proper (T) Element of bool the carrier of T

([#] T) \ c

[#] ( the carrier of T, the of T) is non proper (( the carrier of T, the of T)) Element of bool the carrier of ( the carrier of T, the of T)

([#] ( the carrier of T, the of T)) \ c

the of ( the carrier of T, the of T) is non empty Element of bool (bool the carrier of ( the carrier of T, the of T))

bool (bool the carrier of ( the carrier of T, the of T)) is non empty set

T is () ()

the carrier of T is set

c

the carrier of c

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

the of T is non empty Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () () ()

the carrier of ( the carrier of T, the of T) is set

[: the carrier of ( the carrier of T, the of T), the carrier of c

bool [: the carrier of ( the carrier of T, the of T), the carrier of c

y is V7() V10( the carrier of T) V11( the carrier of c

Q is V7() V10( the carrier of ( the carrier of T, the of T)) V11( the carrier of c

bool the carrier of c

h is Element of bool the carrier of c

Q " h is Element of bool the carrier of ( the carrier of T, the of T)

bool the carrier of ( the carrier of T, the of T) is non empty set

y " h is Element of bool the carrier of T

bool the carrier of c

h is Element of bool the carrier of c

y " h is Element of bool the carrier of T

Q " h is Element of bool the carrier of ( the carrier of T, the of T)

bool the carrier of ( the carrier of T, the of T) is non empty set

T is () ()

the carrier of T is set

c

the carrier of c

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

the of c

bool the carrier of c

bool (bool the carrier of c

( the carrier of c

the carrier of ( the carrier of c

[: the carrier of T, the carrier of ( the carrier of c

bool [: the carrier of T, the carrier of ( the carrier of c

y is V7() V10( the carrier of T) V11( the carrier of c

Q is V7() V10( the carrier of T) V11( the carrier of ( the carrier of c

bool the carrier of ( the carrier of c

h is Element of bool the carrier of ( the carrier of c

Q " h is Element of bool the carrier of T

bool the carrier of T is non empty set

P is Element of bool the carrier of c

h is Element of bool the carrier of c

y " h is Element of bool the carrier of T

bool the carrier of T is non empty set

bool the carrier of ( the carrier of c

P is Element of bool the carrier of ( the carrier of c

T is () ()

the carrier of T is set

c

the carrier of c

[: the carrier of T, the carrier of c

bool [: the carrier of T, the carrier of c

the of T is non empty Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () () ()

the carrier of ( the carrier of T, the of T) is set

the of c

bool the carrier of c

bool (bool the carrier of c

( the carrier of c

the carrier of ( the carrier of c

[: the carrier of ( the carrier of T, the of T), the carrier of ( the carrier of c

bool [: the carrier of ( the carrier of T, the of T), the carrier of ( the carrier of c

y is V7() V10( the carrier of T) V11( the carrier of c

Q is V7() V10( the carrier of ( the carrier of T, the of T)) V11( the carrier of ( the carrier of c

[: the carrier of T, the carrier of ( the carrier of c

bool [: the carrier of T, the carrier of ( the carrier of c

h is V7() V10( the carrier of T) V11( the carrier of ( the carrier of c

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

(T,c

T is ()

c

the carrier of c

the of c

bool the carrier of c

bool (bool the carrier of c

( the carrier of c

[#] T is non proper Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

[#] c

[#] ( the carrier of c

the carrier of ( the carrier of c

bool the carrier of ( the carrier of c

the of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

the of ( the carrier of c

bool (bool the carrier of ( the carrier of c

y is Element of bool the carrier of T

Q is Element of bool the carrier of ( the carrier of c

Q /\ ([#] T) is Element of bool the carrier of T

[#] T is non proper Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

[#] ( the carrier of c

the carrier of ( the carrier of c

bool the carrier of ( the carrier of c

[#] c

the of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

y is Element of bool the carrier of T

Q is Element of bool the carrier of c

Q /\ ([#] T) is Element of bool the carrier of T

T is ()

the carrier of T is set

bool the carrier of T is non empty set

the of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

( the carrier of T, the of T) is () ()

the carrier of ( the carrier of T, the of T) is set

bool the carrier of ( the carrier of T, the of T) is non empty set

c

(T,c

the carrier of (T,c

the of (T,c

bool the carrier of (T,c

bool (bool the carrier of (T,c

( the carrier of (T,c

y is Element of bool the carrier of ( the carrier of T, the of T)

(( the carrier of T, the of T),y) is () (( the carrier of T, the of T))

[#] ( the carrier of (T,c

the carrier of ( the carrier of (T,c

bool the carrier of ( the carrier of (T,c

the () is ()

{} the () is empty Element of bool the carrier of the ()

the carrier of the () is set

bool the carrier of the () is non empty set

( the (),({} the ())) is empty trivial V46() {} -element () ( the ())

T is non empty set

bool T is non empty set

bool (bool T) is non empty set

c

(T,c

T is ()

the carrier of T is set

bool the carrier of T is non empty set

c

y is Element of the carrier of T

the () () is () ()

{} the () () is empty ( the () ()) Element of bool the carrier of the () ()

the carrier of the () () is set

bool the carrier of the () () is non empty set

( the () (),({} the () ())) is empty trivial V46() {} -element () () () ( the () ())