:: 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₂ is Element of bool (bool T)
(T,c₂) is () ()
the carrier of (T,c₂) is set
the of (T,c₂) is Element of bool (bool the carrier of (T,c₂))
bool the carrier of (T,c₂) is non empty set
bool (bool the carrier of (T,c₂)) is non empty set
T is non empty set
bool T is non empty set
bool (bool T) is non empty set
c₂ is Element of bool (bool T)
(T,c₂) is () ()
the carrier of (T,c₂) is set
the of (T,c₂) is Element of bool (bool the carrier of (T,c₂))
bool the carrier of (T,c₂) is non empty set
bool (bool the carrier of (T,c₂)) is non empty set
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₂ is Element of bool (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₂ is Element of bool the carrier of T
c₂ ` is Element of bool the carrier of T
the carrier of T \ c<sub>2</sub> is set
c<sub>2</sub> \/ (c<sub>2</sub> `) is Element of bool the carrier of T
[#] 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₂ is Element of bool the carrier of T
([#] T) \ c₂ is Element of bool the carrier of T
([#] T) \ (([#] T) \ c₂) is Element of bool the carrier of T
c₂ /\ ([#] T) is 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₂ is Element of bool the carrier of T
([#] T) \ c₂ is 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₂ is Element of bool the carrier of T
y is Element of bool the carrier of T
c₂ \/ y is Element of bool the carrier of T
([#] T) \ c₂ is Element of bool the carrier of T
y \ c₂ is Element of bool the carrier of T
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<sub>2</sub> 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
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<sub>2</sub> is (T)
the carrier of c<sub>2</sub> is set
[#] 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<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
([#] T) /\ the carrier of c<sub>2</sub> is Element of bool the carrier of T
the of c<sub>2</sub> is Element of bool (bool the carrier of c<sub>2</sub>)
bool (bool the carrier of c<sub>2</sub>) is non empty set
Q is Element of bool (bool the carrier of c<sub>2</sub>)
union Q is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub> is Element of bool the carrier of T
P is set
Q is set
Q /\ the carrier of c<sub>2</sub> is set
P is set
P is set
Q is set
Q is Element of bool the carrier of T
Q /\ the carrier of c<sub>2</sub> is Element of bool the carrier of T
Q is Element of bool the carrier of c<sub>2</sub>
h is Element of bool the carrier of c<sub>2</sub>
Q /\ h is Element of bool the carrier of c<sub>2</sub>
P is Element of bool the carrier of T
P /\ the carrier of c<sub>2</sub> is Element of bool the carrier of T
Q is Element of bool the carrier of T
Q /\ the carrier of c<sub>2</sub> is Element of bool the carrier of T
(Q /\ the carrier of c<sub>2</sub>) /\ the carrier of c<sub>2</sub> is Element of bool the carrier of T
P /\ ((Q /\ the carrier of c<sub>2</sub>) /\ the carrier of c<sub>2</sub>) is Element of bool the carrier of T
the carrier of c<sub>2</sub> /\ the carrier of c<sub>2</sub> is set
Q /\ ( the carrier of c<sub>2</sub> /\ the carrier of c<sub>2</sub>) is Element of bool the carrier of T
P /\ (Q /\ ( the carrier of c<sub>2</sub> /\ the carrier of c<sub>2</sub>)) is Element of bool the carrier of T
P /\ Q is Element of bool the carrier of T
(P /\ Q) /\ the carrier of c<sub>2</sub> 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<sub>2</sub> is Element of bool the carrier of T
the of T is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
bool c<sub>2</sub> is non empty set
bool (bool c<sub>2</sub>) is non empty set
y is Element of bool (bool c<sub>2</sub>)
Q is Element of bool (bool c<sub>2</sub>)
(c<sub>2</sub>,Q) is () ()
the carrier of (c<sub>2</sub>,Q) is set
bool the carrier of (c<sub>2</sub>,Q) is non empty set
[#] (c<sub>2</sub>,Q) is non proper Element of bool the carrier of (c<sub>2</sub>,Q)
P is Element of bool the carrier of (c<sub>2</sub>,Q)
Q is Element of bool the carrier of T
Q /\ c<sub>2</sub> is Element of bool the carrier of T
Q is Element of bool the carrier of T
Q /\ ([#] (c<sub>2</sub>,Q)) is Element of bool the carrier of (c<sub>2</sub>,Q)
[#] 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<sub>2</sub> is non empty Element of bool the carrier of T
(T,c<sub>2</sub>) is () (T)
[#] (T,c<sub>2</sub>) is non proper Element of bool the carrier of (T,c<sub>2</sub>)
the carrier of (T,c<sub>2</sub>) is set
bool the carrier of (T,c<sub>2</sub>) is non empty set
T is () ()
the () () (T) is () () (T)
T is () ()
the carrier of T is set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is () () (T)
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<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is () () (T)
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<sub>2</sub> is Element of bool the carrier of T
P /\ (y /\ c<sub>2</sub>) is Element of bool the carrier of T
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<sub>2</sub>) is Element of bool the carrier of T
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<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is () (T)
the carrier of (T,c<sub>2</sub>) is set
[#] (T,c<sub>2</sub>) is non proper Element of bool the carrier of (T,c<sub>2</sub>)
bool the carrier of (T,c<sub>2</sub>) is non empty set
T is ()
the carrier of T is set
bool the carrier of T is non empty set
c<sub>2</sub> is non empty ()
the carrier of c<sub>2</sub> is non empty set
[: the carrier of T, the carrier of c<sub>2</sub>:] is set
bool [: the carrier of T, the carrier of c<sub>2</sub>:] is non empty set
y is V7() V10( the carrier of T) V11( the carrier of c<sub>2</sub>) V12() V21( the carrier of T, the carrier of c<sub>2</sub>) Element of bool [: the carrier of T, the carrier of c<sub>2</sub>:]
Q is Element of bool the carrier of T
y | Q is V7() V10( the carrier of T) V11( the carrier of c<sub>2</sub>) Element of bool [: the carrier of T, the carrier of c<sub>2</sub>:]
(T,Q) is () (T)
the carrier of (T,Q) is set
[: the carrier of (T,Q), the carrier of c<sub>2</sub>:] is set
bool [: the carrier of (T,Q), the carrier of c<sub>2</sub>:] is non empty set
T is ()
the carrier of T is set
c<sub>2</sub> is ()
the carrier of c<sub>2</sub> is set
[: the carrier of T, the carrier of c<sub>2</sub>:] is set
bool [: the carrier of T, the carrier of c<sub>2</sub>:] is non empty set
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<sub>2</sub> is ()
the carrier of c<sub>2</sub> is set
the of c<sub>2</sub> is Element of bool (bool the carrier of c<sub>2</sub>)
bool the carrier of c<sub>2</sub> is non empty set
bool (bool the carrier of c<sub>2</sub>) is non empty set
( the carrier of c<sub>2</sub>, the of c<sub>2</sub>) is () ()
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<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
h is Element of bool the carrier of Q
Q is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub> is (T)
the carrier of c<sub>2</sub> is set
bool the carrier of c<sub>2</sub> is non empty set
y is Element of bool the carrier of c<sub>2</sub>
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
[#] 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<sub>2</sub> is Element of bool the carrier of T
the Element of c<sub>2</sub> is Element of c<sub>2</sub>
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<sub>2</sub> is (T)
the carrier of c<sub>2</sub> is set
bool the carrier of c<sub>2</sub> is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
y is Element of bool the carrier of c<sub>2</sub>
([#] c<sub>2</sub>) \ y is Element of bool the carrier of c<sub>2</sub>
the of c<sub>2</sub> is Element of bool (bool the carrier of c<sub>2</sub>)
bool (bool the carrier of c<sub>2</sub>) 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
Q is Element of bool the carrier of T
Q /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
[#] T is non proper Element of bool the carrier of T
([#] T) \ Q is Element of bool the carrier of T
(([#] T) \ Q) /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
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
([#] c<sub>2</sub>) \ Q is Element of bool the carrier of c<sub>2</sub>
([#] c<sub>2</sub>) /\ Q is Element of bool the carrier of T
([#] c<sub>2</sub>) \ (([#] c<sub>2</sub>) /\ Q) is Element of bool the carrier of c<sub>2</sub>
([#] 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<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
([#] T) \ Q is Element of bool the carrier of T
(([#] T) \ Q) /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
([#] c<sub>2</sub>) \ Q is Element of bool the carrier of c<sub>2</sub>
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 is Element of bool the carrier of T
Q /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
h is Element of bool the carrier of T
h /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub> is Element of bool (bool the carrier of T)
meet c<sub>2</sub> is Element of bool the carrier of T
[#] 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<sub>2</sub> is Element of bool the carrier of T
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<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool the carrier of T
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<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool the carrier of T
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<sub>2</sub> is (T)
the carrier of c<sub>2</sub> is set
bool the carrier of c<sub>2</sub> is non empty set
[#] c<sub>2</sub> is non proper Element of bool the carrier of c<sub>2</sub>
y is Element of bool the carrier of T
(T,y) is Element of bool the carrier of T
(T,y) /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
Q is Element of bool the carrier of c<sub>2</sub>
(c<sub>2</sub>,Q) is Element of bool the carrier of c<sub>2</sub>
h is set
Q is Element of bool the carrier of T
Q /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
P is Element of bool the carrier of T
P is Element of bool the carrier of c<sub>2</sub>
Q is Element of bool the carrier of T
Q /\ ([#] c<sub>2</sub>) is Element of bool the carrier of c<sub>2</sub>
T is ()
the carrier of T is set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool the carrier of T
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<sub>2</sub> is Element of bool the carrier of T
y is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool the carrier of T
(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<sub>2</sub> is Element of bool the carrier of T
y is Element of bool the carrier of T
c<sub>2</sub> \/ y is Element of bool the carrier of T
(T,(c<sub>2</sub> \/ y)) is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool the carrier of T
(T,y) is Element of bool the carrier of T
(T,c<sub>2</sub>) \/ (T,y) is Element of bool the carrier of T
Q is set
h is Element of bool the carrier of T
c<sub>2</sub> /\ h is Element of bool the carrier of T
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<sub>2</sub> \/ y) /\ (h /\ P) is Element of bool the carrier of T
c<sub>2</sub> /\ (h /\ P) is Element of bool the carrier of T
P /\ h is Element of bool the carrier of T
y /\ (P /\ h) is Element of bool the carrier of T
(c<sub>2</sub> /\ (h /\ P)) \/ (y /\ (P /\ h)) is Element of bool the carrier of T
(c<sub>2</sub> /\ h) /\ P is Element of bool the carrier of T
((c<sub>2</sub> /\ h) /\ P) \/ (y /\ (P /\ h)) is Element of bool the carrier of T
{} /\ 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<sub>2</sub> is Element of bool the carrier of T
y is Element of bool the carrier of T
c<sub>2</sub> /\ y is Element of bool the carrier of T
(T,(c<sub>2</sub> /\ y)) is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool the carrier of T
(T,y) is Element of bool the carrier of T
(T,c<sub>2</sub>) /\ (T,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<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool the carrier of T
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<sub>2</sub> is Element of bool the carrier of T
([#] T) \ c<sub>2</sub> is Element of bool the carrier of T
(T,(([#] T) \ c<sub>2</sub>)) is Element of bool the carrier of T
([#] T) \ (([#] T) \ c<sub>2</sub>) 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
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<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool the carrier of T
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<sub>2</sub> is non empty (T)
the carrier of c<sub>2</sub> is non empty set
[#] c<sub>2</sub> is non empty non proper Element of bool the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
[#] 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<sub>2</sub>
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<sub>2</sub> is () ()
the carrier of c<sub>2</sub> is set
[: the carrier of T, the carrier of c<sub>2</sub>:] is set
bool [: the carrier of T, the carrier of c<sub>2</sub>:] is non empty set
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<sub>2</sub>) V12() V21( the carrier of T, the carrier of c<sub>2</sub>) Element of bool [: the carrier of T, the carrier of c<sub>2</sub>:]
bool the carrier of c<sub>2</sub> is non empty set
P is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
(rng h) /\ P is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>
h " (((rng h) /\ ([#] y)) /\ P) is Element of bool the carrier of T
([#] y) /\ P is Element of bool the carrier of c<sub>2</sub>
(rng h) /\ (([#] y) /\ P) is Element of bool the carrier of c<sub>2</sub>
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<sub>2</sub>)
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<sub>2</sub> is non empty () ()
the carrier of c<sub>2</sub> is non empty set
[: the carrier of T, the carrier of c<sub>2</sub>:] is set
bool [: the carrier of T, the carrier of c<sub>2</sub>:] is non empty set
y is V7() V10( the carrier of T) V11( the carrier of c<sub>2</sub>) V12() V21( the carrier of T, the carrier of c<sub>2</sub>) Element of bool [: the carrier of T, the carrier of c<sub>2</sub>:]
Q is () (c<sub>2</sub>)
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<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
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<sub>2</sub>
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<sub>2</sub> is Element of bool the carrier of T
{} 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<sub>2</sub> is Element of bool the carrier of T
c<sub>2</sub> is non empty ()
the carrier of c<sub>2</sub> is non empty set
T is () ()
y is Element of the carrier of c<sub>2</sub>
T --> y is V7() V10( the carrier of T) V11( the carrier of c<sub>2</sub>) V12() V21( the carrier of T, the carrier of c<sub>2</sub>) Element of bool [: the carrier of T, the carrier of c<sub>2</sub>:]
the carrier of T is set
[: the carrier of T, the carrier of c<sub>2</sub>:] is set
bool [: the carrier of T, the carrier of c<sub>2</sub>:] is non empty set
K119( the carrier of c<sub>2</sub>, the carrier of T,y) is V7() V10( the carrier of T) V11( the carrier of c<sub>2</sub>) V12() V21( the carrier of T, the carrier of c<sub>2</sub>) Element of bool [: the carrier of T, the carrier of c<sub>2</sub>:]
bool the carrier of c<sub>2</sub> is non empty set
Q is Element of bool the carrier of c<sub>2</sub>
(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<sub>2</sub> is non empty () ()
the carrier of c<sub>2</sub> is non empty set
[: the carrier of T, the carrier of c<sub>2</sub>:] is set
bool [: the carrier of T, the carrier of c<sub>2</sub>:] is non empty set
the Element of the carrier of c<sub>2</sub> is Element of the carrier of c<sub>2</sub>
T --> the Element of the carrier of c<sub>2</sub> is V7() V10( the carrier of T) V11( the carrier of c<sub>2</sub>) V12() V21( the carrier of T, the carrier of c<sub>2</sub>) (T,c<sub>2</sub>) Element of bool [: the carrier of T, the carrier of c<sub>2</sub>:]
K119( the carrier of c<sub>2</sub>, the carrier of T, the Element of the carrier of c<sub>2</sub>) is V7() V10( the carrier of T) V11( the carrier of c<sub>2</sub>) V12() V21( the carrier of T, the carrier of c<sub>2</sub>) Element of bool [: the carrier of T, the carrier of c<sub>2</sub>:]
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<sub>2</sub> is Element of bool (bool the carrier of (1,([#] (bool 1))))
union c<sub>2</sub> is Element of bool the carrier of (1,([#] (bool 1)))
c<sub>2</sub> is Element of bool the carrier of (1,([#] (bool 1)))
y is Element of bool the carrier of (1,([#] (bool 1)))
c<sub>2</sub> /\ y is Element of bool the carrier of (1,([#] (bool 1)))
c<sub>2</sub> is non empty () ()
the carrier of c<sub>2</sub> is non empty set
y is Element of the carrier of c<sub>2</sub>
Q is Element of the carrier of c<sub>2</sub>
bool the carrier of c<sub>2</sub> is non empty set
T is ()
the carrier of T is set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of the carrier of T
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₂ is Element of the carrier of T
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₂ is (( the carrier of T, the of T))
[#] c₂ is non proper Element of bool the carrier of c₂
the carrier of c₂ is set
bool the carrier of c₂ is non empty set
[#] ( 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₂ is Element of bool (bool the carrier of c₂)
bool (bool the carrier of c₂) is non empty set
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₂) is Element of bool the carrier of 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₂ is set
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₂ is set
[#] T is non proper (T) Element of bool the carrier of T
([#] T) \ c₂ is Element of bool the carrier of T
[#] ( 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₂ is Element of bool the carrier of ( the carrier of T, the of T)
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₂ is () ()
the carrier of c₂ is set
[: the carrier of T, the carrier of c₂:] is set
bool [: the carrier of T, the carrier of c₂:] is non empty 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 carrier of ( the carrier of T, the of T), the carrier of c₂:] is set
bool [: the carrier of ( the carrier of T, the of T), the carrier of c₂:] is non empty set
y is V7() V10( the carrier of T) V11( the carrier of c₂) V12() V21( the carrier of T, the carrier of c₂) Element of bool [: the carrier of T, the carrier of c₂:]
Q is V7() V10( the carrier of ( the carrier of T, the of T)) V11( the carrier of c₂) V12() V21( the carrier of ( the carrier of T, the of T), the carrier of c₂) Element of bool [: the carrier of ( the carrier of T, the of T), the carrier of c₂:]
bool the carrier of c₂ is non empty set
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₂ is non empty set
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₂ is () ()
the carrier of c₂ is set
[: the carrier of T, the carrier of c₂:] is set
bool [: the carrier of T, the carrier of c₂:] is non empty set
the of c₂ is non empty Element of bool (bool the carrier of c₂)
bool the carrier of c₂ is non empty set
bool (bool the carrier of c₂) is non empty set
( the carrier of c₂, the of c₂) is () () ()
the carrier of ( the carrier of c₂, the of c₂) is set
[: the carrier of T, the carrier of ( the carrier of c₂, the of c₂):] is set
bool [: the carrier of T, the carrier of ( the carrier of c₂, the of c₂):] is non empty set
y is V7() V10( the carrier of T) V11( the carrier of c₂) V12() V21( the carrier of T, the carrier of c₂) Element of bool [: the carrier of T, the carrier of c₂:]
Q is V7() V10( the carrier of T) V11( the carrier of ( the carrier of c₂, the of c₂)) V12() V21( the carrier of T, the carrier of ( the carrier of c₂, the of c₂)) Element of bool [: the carrier of T, the carrier of ( the carrier of c₂, the of c₂):]
bool the carrier of ( the carrier of c₂, the of c₂) is non empty set
h is Element of bool the carrier of ( the carrier of c₂, the 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₂, the of c₂) is non empty set
P is Element of bool the carrier of ( the carrier of c₂, the of c₂)
T is () ()
the carrier of T is set
c₂ is () ()
the carrier of c₂ is set
[: the carrier of T, the carrier of c₂:] is set
bool [: the carrier of T, the carrier of c₂:] is non empty 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 c₂ is non empty Element of bool (bool the carrier of c₂)
bool the carrier of c₂ is non empty set
bool (bool the carrier of c₂) is non empty set
( the carrier of c₂, the of c₂) is () () ()
the carrier of ( the carrier of c₂, the of c₂) is set
[: the carrier of ( the carrier of T, the of T), the carrier of ( the carrier of c₂, the of c₂):] is set
bool [: the carrier of ( the carrier of T, the of T), the carrier of ( the carrier of c₂, the of c₂):] is non empty set
y is V7() V10( the carrier of T) V11( the carrier of c₂) V12() V21( the carrier of T, the carrier of c₂) Element of bool [: the carrier of T, 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 of c₂)) V12() V21( the carrier of ( the carrier of T, the of T), the carrier of ( the carrier of c₂, the of c₂)) Element of bool [: the carrier of ( the carrier of T, the of T), the carrier of ( the carrier of c₂, the of c₂):]
[: the carrier of T, the carrier of ( the carrier of c₂, the of c₂):] is set
bool [: the carrier of T, the carrier of ( the carrier of c₂, the of c₂):] is non empty set
h is V7() V10( the carrier of T) V11( the carrier of ( the carrier of c₂, the of c₂)) V12() V21( the carrier of T, the carrier of ( the carrier of c₂, the of c₂)) Element of bool [: the carrier of T, the carrier of ( the carrier of c₂, the of c₂):]
T is ()
the carrier of T is set
bool the carrier of T is non empty set
c₂ is empty Element of bool the carrier of T
(T,c₂) is () (T)
T is ()
c₂ is ()
the carrier of c₂ is set
the of c₂ is Element of bool (bool the carrier of c₂)
bool the carrier of c₂ is non empty set
bool (bool the carrier of c₂) is non empty set
( the carrier of c₂, the of c₂) 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
[#] c₂ is non proper Element of bool the carrier of c₂
[#] ( the carrier of c₂, the of c₂) is non proper Element of bool the carrier of ( the carrier of c₂, the of c₂)
the carrier of ( the carrier of c₂, the of c₂) is set
bool the carrier of ( the carrier of c₂, the of c₂) 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 of ( the carrier of c₂, the of c₂) is Element of bool (bool the carrier of ( the carrier of c₂, the of c₂))
bool (bool the carrier of ( the carrier of c₂, the of c₂)) is non empty set
y is Element of bool the carrier of T
Q is Element of bool the carrier of ( the carrier of c₂, the 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 of c₂) is non proper Element of bool the carrier of ( the carrier of c₂, the of c₂)
the carrier of ( the carrier of c₂, the of c₂) is set
bool the carrier of ( the carrier of c₂, the of c₂) is non empty set
[#] c₂ is non proper Element of 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
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₂ is Element of bool the carrier of T
(T,c₂) is () (T)
the carrier of (T,c₂) is set
the of (T,c₂) is Element of bool (bool the carrier of (T,c₂))
bool the carrier of (T,c₂) is non empty set
bool (bool the carrier of (T,c₂)) is non empty set
( the carrier of (T,c₂), the of (T,c₂)) is () ()
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 of (T,c₂)) is non proper Element of bool the carrier of ( the carrier of (T,c₂), the of (T,c₂))
the carrier of ( the carrier of (T,c₂), the of (T,c₂)) is set
bool the carrier of ( the carrier of (T,c₂), the of (T,c₂)) is non empty set
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₂ is Element of bool (bool T)
(T,c₂) is () ()
T is ()
the carrier of T is set
bool the carrier of T is non empty set
c₂ is Element of the carrier of T
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 () ())