:: YELLOW12 semantic presentation

the carrier of K259() is non empty set
K165() is Element of bool K161()
K161() is set
bool K161() is non empty set
K103() is set
bool K103() is non empty set

the empty set is empty set
1 is non empty set
{{},1} is non empty set

the carrier of K219() is non empty set
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],K161():] is set
bool [:[:1,1:],K161():] is non empty set
[:K161(),K161():] is set
[:[:K161(),K161():],K161():] is set
bool [:[:K161(),K161():],K161():] is non empty set
2 is non empty set
[:2,2:] is non empty set
[:[:2,2:],K161():] is set
bool [:[:2,2:],K161():] is non empty set
K247() is V99() L7()
bool K165() is non empty set

is non empty set
S1 is empty set
union S1 is set
T1 is set
S1 is set
T2 is set
S2 is set
pr2 (S1,S2) is Relation-like [:S1,S2:] -defined S2 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S2:]
[:S1,S2:] is set
[:[:S1,S2:],S2:] is set
bool [:[:S1,S2:],S2:] is non empty set
pr1 (S1,S2) is Relation-like [:S1,S2:] -defined S1 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S1:]
[:[:S1,S2:],S1:] is set
bool [:[:S1,S2:],S1:] is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> is Relation-like Function-like set
dom <:(pr2 (S1,S2)),(pr1 (S1,S2)):> is set
dom (pr2 (S1,S2)) is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
bool [:S1,S2:] is non empty set
dom (pr1 (S1,S2)) is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
(dom (pr2 (S1,S2))) /\ (dom (pr1 (S1,S2))) is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
(dom (pr2 (S1,S2))) /\ [:S1,S2:] is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
[:S1,S2:] /\ [:S1,S2:] is set
[T1,T2] is set
{T1,T2} is non empty set
{T1} is non empty set
{{T1,T2},{T1}} is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . (T1,T2) is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . [T1,T2] is set
(pr2 (S1,S2)) . (T1,T2) is set
(pr2 (S1,S2)) . [T1,T2] is set
(pr1 (S1,S2)) . (T1,T2) is set
(pr1 (S1,S2)) . [T1,T2] is set
[((pr2 (S1,S2)) . (T1,T2)),((pr1 (S1,S2)) . (T1,T2))] is set
{((pr2 (S1,S2)) . (T1,T2)),((pr1 (S1,S2)) . (T1,T2))} is non empty set
{((pr2 (S1,S2)) . (T1,T2))} is non empty set
{{((pr2 (S1,S2)) . (T1,T2)),((pr1 (S1,S2)) . (T1,T2))},{((pr2 (S1,S2)) . (T1,T2))}} is non empty set
[T2,((pr1 (S1,S2)) . (T1,T2))] is set
{T2,((pr1 (S1,S2)) . (T1,T2))} is non empty set
{T2} is non empty set
{{T2,((pr1 (S1,S2)) . (T1,T2))},{T2}} is non empty set
[T2,T1] is set
{T2,T1} is non empty set
{{T2,T1},{T2}} is non empty set
S1 is set
[:S1,S1:] is set
delta S1 is Relation-like S1 -defined [:S1,S1:] -valued Function-like quasi_total Element of bool [:S1,[:S1,S1:]:]
[:S1,[:S1,S1:]:] is set
bool [:S1,[:S1,S1:]:] is non empty set
S2 is set
(delta S1) .: S2 is Relation-like S1 -defined S1 -valued Element of bool [:S1,S1:]
bool [:S1,S1:] is non empty set
[:S2,S2:] is set
T2 is set
dom (delta S1) is Element of bool S1
bool S1 is non empty set
R1 is set
(delta S1) . R1 is set
[R1,R1] is set
{R1,R1} is non empty set
{R1} is non empty set
{{R1,R1},{R1}} is non empty set
S1 is set
[:S1,S1:] is set
delta S1 is Relation-like S1 -defined [:S1,S1:] -valued Function-like quasi_total Element of bool [:S1,[:S1,S1:]:]
[:S1,[:S1,S1:]:] is set
bool [:S1,[:S1,S1:]:] is non empty set
S2 is set
[:S2,S2:] is set
(delta S1) " [:S2,S2:] is Element of bool S1
bool S1 is non empty set
T2 is set
(delta S1) . T2 is set
[T2,T2] is set
{T2,T2} is non empty set
{T2} is non empty set
{{T2,T2},{T2}} is non empty set
S1 is set
bool S1 is non empty set
[:S1,S1:] is set
delta S1 is Relation-like S1 -defined [:S1,S1:] -valued Function-like quasi_total Element of bool [:S1,[:S1,S1:]:]
[:S1,[:S1,S1:]:] is set
bool [:S1,[:S1,S1:]:] is non empty set
S2 is Element of bool S1
[:S2,S2:] is Relation-like S1 -defined S1 -valued Element of bool [:S1,S1:]
bool [:S1,S1:] is non empty set
(delta S1) " [:S2,S2:] is Element of bool S1
T2 is set
(delta S1) . T2 is set
[T2,T2] is set
{T2,T2} is non empty set
{T2} is non empty set
{{T2,T2},{T2}} is non empty set
dom (delta S1) is Element of bool S1
S1 is set
S2 is set
pr2 (S1,S2) is Relation-like [:S1,S2:] -defined S2 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S2:]
[:S1,S2:] is set
[:[:S1,S2:],S2:] is set
bool [:[:S1,S2:],S2:] is non empty set
pr1 (S1,S2) is Relation-like [:S1,S2:] -defined S1 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S1:]
[:[:S1,S2:],S1:] is set
bool [:[:S1,S2:],S1:] is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> is Relation-like Function-like set
dom <:(pr2 (S1,S2)),(pr1 (S1,S2)):> is set
rng <:(pr2 (S1,S2)),(pr1 (S1,S2)):> is set
[:S2,S1:] is set
dom (pr2 (S1,S2)) is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
bool [:S1,S2:] is non empty set
dom (pr1 (S1,S2)) is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
(dom (pr2 (S1,S2))) /\ (dom (pr1 (S1,S2))) is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
(dom (pr2 (S1,S2))) /\ [:S1,S2:] is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
[:S1,S2:] /\ [:S1,S2:] is set
rng (pr2 (S1,S2)) is Element of bool S2
bool S2 is non empty set
rng (pr1 (S1,S2)) is Element of bool S1
bool S1 is non empty set
[:(rng (pr2 (S1,S2))),(rng (pr1 (S1,S2))):] is Relation-like S2 -defined S1 -valued Element of bool [:S2,S1:]
bool [:S2,S1:] is non empty set
T2 is set
R1 is set
R2 is set
[R1,R2] is set
{R1,R2} is non empty set
{R1} is non empty set
{{R1,R2},{R1}} is non empty set
[R2,R1] is set
{R2,R1} is non empty set
{R2} is non empty set
{{R2,R1},{R2}} is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . (R2,R1) is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . [R2,R1] is set
S1 is set
S2 is set
pr2 (S1,S2) is Relation-like [:S1,S2:] -defined S2 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S2:]
[:S1,S2:] is set
[:[:S1,S2:],S2:] is set
bool [:[:S1,S2:],S2:] is non empty set
pr1 (S1,S2) is Relation-like [:S1,S2:] -defined S1 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S1:]
[:[:S1,S2:],S1:] is set
bool [:[:S1,S2:],S1:] is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> is Relation-like Function-like set
T1 is set
T2 is set
[:T1,T2:] is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> .: [:T1,T2:] is set
[:T2,T1:] is set
R2 is set
dom <:(pr2 (S1,S2)),(pr1 (S1,S2)):> is set
R is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . R is set
C is set
BT is set
[C,BT] is set
{C,BT} is non empty set
{C} is non empty set
{{C,BT},{C}} is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . (C,BT) is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . [C,BT] is set
[BT,C] is set
{BT,C} is non empty set
{BT} is non empty set
{{BT,C},{BT}} is non empty set
S1 is set
bool S1 is non empty set
S2 is set
bool S2 is non empty set
pr2 (S1,S2) is Relation-like [:S1,S2:] -defined S2 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S2:]
[:S1,S2:] is set
[:[:S1,S2:],S2:] is set
bool [:[:S1,S2:],S2:] is non empty set
pr1 (S1,S2) is Relation-like [:S1,S2:] -defined S1 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S1:]
[:[:S1,S2:],S1:] is set
bool [:[:S1,S2:],S1:] is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> is Relation-like Function-like set
T1 is Element of bool S1
T2 is Element of bool S2
[:T1,T2:] is Relation-like S1 -defined S2 -valued Element of bool [:S1,S2:]
bool [:S1,S2:] is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> .: [:T1,T2:] is set
[:T2,T1:] is Relation-like S2 -defined S1 -valued Element of bool [:S2,S1:]
[:S2,S1:] is set
bool [:S2,S1:] is non empty set
dom <:(pr2 (S1,S2)),(pr1 (S1,S2)):> is set
R2 is set
R is set
C is set
[R,C] is set
{R,C} is non empty set
{R} is non empty set
{{R,C},{R}} is non empty set
[C,R] is set
{C,R} is non empty set
{C} is non empty set
{{C,R},{C}} is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . (C,R) is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . [C,R] is set
S1 is set
S2 is set
pr2 (S1,S2) is Relation-like [:S1,S2:] -defined S2 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S2:]
[:S1,S2:] is set
[:[:S1,S2:],S2:] is set
bool [:[:S1,S2:],S2:] is non empty set
pr1 (S1,S2) is Relation-like [:S1,S2:] -defined S1 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S1:]
[:[:S1,S2:],S1:] is set
bool [:[:S1,S2:],S1:] is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> is Relation-like Function-like set
T2 is set
dom <:(pr2 (S1,S2)),(pr1 (S1,S2)):> is set
R1 is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . T2 is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . R1 is set
R2 is set
R is set
[R2,R] is set
{R2,R} is non empty set
{R2} is non empty set
{{R2,R},{R2}} is non empty set
C is set
BT is set
[C,BT] is set
{C,BT} is non empty set
{C} is non empty set
{{C,BT},{C}} is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . (C,BT) is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . [C,BT] is set
[BT,C] is set
{BT,C} is non empty set
{BT} is non empty set
{{BT,C},{BT}} is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . (R2,R) is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . [R2,R] is set
[R,R2] is set
{R,R2} is non empty set
{R} is non empty set
{{R,R2},{R}} is non empty set
S1 is set
S2 is set
pr2 (S1,S2) is Relation-like [:S1,S2:] -defined S2 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S2:]
[:S1,S2:] is set
[:[:S1,S2:],S2:] is set
bool [:[:S1,S2:],S2:] is non empty set
pr1 (S1,S2) is Relation-like [:S1,S2:] -defined S1 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S1:]
[:[:S1,S2:],S1:] is set
bool [:[:S1,S2:],S1:] is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> is Relation-like Function-like set
S1 is set
S2 is set
pr2 (S1,S2) is Relation-like [:S1,S2:] -defined S2 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S2:]
[:S1,S2:] is set
[:[:S1,S2:],S2:] is set
bool [:[:S1,S2:],S2:] is non empty set
pr1 (S1,S2) is Relation-like [:S1,S2:] -defined S1 -valued Function-like quasi_total Element of bool [:[:S1,S2:],S1:]
[:[:S1,S2:],S1:] is set
bool [:[:S1,S2:],S1:] is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> is Relation-like Function-like one-to-one set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> " is Relation-like Function-like set
pr2 (S2,S1) is Relation-like [:S2,S1:] -defined S1 -valued Function-like quasi_total Element of bool [:[:S2,S1:],S1:]
[:S2,S1:] is set
[:[:S2,S1:],S1:] is set
bool [:[:S2,S1:],S1:] is non empty set
pr1 (S2,S1) is Relation-like [:S2,S1:] -defined S2 -valued Function-like quasi_total Element of bool [:[:S2,S1:],S2:]
[:[:S2,S1:],S2:] is set
bool [:[:S2,S1:],S2:] is non empty set
<:(pr2 (S2,S1)),(pr1 (S2,S1)):> is Relation-like Function-like one-to-one set
dom (<:(pr2 (S1,S2)),(pr1 (S1,S2)):> ") is set
rng <:(pr2 (S1,S2)),(pr1 (S1,S2)):> is set
R1 is set
R2 is set
R is set
[R2,R] is set
{R2,R} is non empty set
{R2} is non empty set
{{R2,R},{R2}} is non empty set
<:(pr2 (S2,S1)),(pr1 (S2,S1)):> . (R2,R) is set
<:(pr2 (S2,S1)),(pr1 (S2,S1)):> . [R2,R] is set
[R,R2] is set
{R,R2} is non empty set
{R} is non empty set
{{R,R2},{R}} is non empty set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . (R,R2) is set
<:(pr2 (S1,S2)),(pr1 (S1,S2)):> . [R,R2] is set
dom <:(pr2 (S1,S2)),(pr1 (S1,S2)):> is set
(<:(pr2 (S1,S2)),(pr1 (S1,S2)):> ") . R1 is set
<:(pr2 (S2,S1)),(pr1 (S2,S1)):> . R1 is set
dom <:(pr2 (S2,S1)),(pr1 (S2,S1)):> is set

the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty RelStr
the carrier of S2 is non empty set
the InternalRel of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of the carrier of S1
T2 is Element of the carrier of S1
T1 "/\" T2 is Element of the carrier of S1
R1 is Element of the carrier of S2
R2 is Element of the carrier of S2
R1 "/\" R2 is Element of the carrier of S2
{T1,T2} is non empty Element of bool the carrier of S1
bool the carrier of S1 is non empty set
"/\" ({T1,T2},S1) is Element of the carrier of S1
{R1,R2} is non empty Element of bool the carrier of S2
bool the carrier of S2 is non empty set
"/\" ({R1,R2},S2) is Element of the carrier of S2

the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty RelStr
the carrier of S2 is non empty set
the InternalRel of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of the carrier of S1
T2 is Element of the carrier of S1
T1 "\/" T2 is Element of the carrier of S1
R1 is Element of the carrier of S2
R2 is Element of the carrier of S2
R1 "\/" R2 is Element of the carrier of S2
{T1,T2} is non empty Element of bool the carrier of S1
bool the carrier of S1 is non empty set
"\/" ({T1,T2},S1) is Element of the carrier of S1
{R1,R2} is non empty Element of bool the carrier of S2
bool the carrier of S2 is non empty set
"\/" ({R1,R2},S2) is Element of the carrier of S2

the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty RelStr
the carrier of S2 is non empty set
bool the carrier of S2 is non empty set
the InternalRel of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of bool the carrier of S1
T2 is Element of bool the carrier of S1
T1 "/\" T2 is Element of bool the carrier of S1
R1 is Element of bool the carrier of S2
R2 is Element of bool the carrier of S2
R1 "/\" R2 is Element of bool the carrier of S2
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of S1 : ( b1 in T1 & b2 in T2 ) } is set
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of S2 : ( b1 in R1 & b2 in R2 ) } is set
BT is set
BS is Element of the carrier of S1
Bpr is Element of the carrier of S1
BS "/\" Bpr is Element of the carrier of S1
c is Element of the carrier of S2
a is Element of the carrier of S2
c "/\" a is Element of the carrier of S2
BT is set
BS is Element of the carrier of S2
Bpr is Element of the carrier of S2
BS "/\" Bpr is Element of the carrier of S2
c is Element of the carrier of S1
a is Element of the carrier of S1
c "/\" a is Element of the carrier of S1

the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty RelStr
the carrier of S2 is non empty set
bool the carrier of S2 is non empty set
the InternalRel of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of bool the carrier of S1
T2 is Element of bool the carrier of S1
T1 "\/" T2 is Element of bool the carrier of S1
R1 is Element of bool the carrier of S2
R2 is Element of bool the carrier of S2
R1 "\/" R2 is Element of bool the carrier of S2
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of S1 : ( b1 in T1 & b2 in T2 ) } is set
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of S2 : ( b1 in R1 & b2 in R2 ) } is set
BT is set
BS is Element of the carrier of S1
Bpr is Element of the carrier of S1
BS "\/" Bpr is Element of the carrier of S1
c is Element of the carrier of S2
a is Element of the carrier of S2
c "\/" a is Element of the carrier of S2
BT is set
BS is Element of the carrier of S2
Bpr is Element of the carrier of S2
BS "\/" Bpr is Element of the carrier of S2
c is Element of the carrier of S1
a is Element of the carrier of S1
c "\/" a is Element of the carrier of S1
S1 is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty reflexive non void RelStr
the carrier of S2 is non empty set
the InternalRel of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of the carrier of S1
waybelow T1 is Element of bool the carrier of S1
bool the carrier of S1 is non empty set
{ b1 where b1 is Element of the carrier of S1 : b1 is_way_below T1 } is set
wayabove T1 is Element of bool the carrier of S1
{ b1 where b1 is Element of the carrier of S1 : T1 is_way_below b1 } is set
T2 is Element of the carrier of S2
waybelow T2 is Element of bool the carrier of S2
bool the carrier of S2 is non empty set
{ b1 where b1 is Element of the carrier of S2 : b1 is_way_below T2 } is set
wayabove T2 is Element of bool the carrier of S2
{ b1 where b1 is Element of the carrier of S2 : T2 is_way_below b1 } is set
R1 is set
R2 is Element of the carrier of S1
R is Element of the carrier of S2
R1 is set
R2 is Element of the carrier of S2
R is Element of the carrier of S1
R1 is set
R2 is Element of the carrier of S1
R is Element of the carrier of S2
R1 is set
R2 is Element of the carrier of S2
R is Element of the carrier of S1

the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty reflexive non void RelStr
the carrier of S2 is non empty set
the InternalRel of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
bool the carrier of S2 is non empty set
T1 is Element of the carrier of S2
{T1} is non empty Element of bool the carrier of S2
T2 is non empty directed Element of bool the carrier of S2
"\/" (T2,S2) is Element of the carrier of S2
T1 "/\" ("\/" (T2,S2)) is Element of the carrier of S2
{T1} "/\" T2 is non empty Element of bool the carrier of S2
"\/" (({T1} "/\" T2),S2) is Element of the carrier of S2
bool the carrier of S1 is non empty set
R2 is Element of the carrier of S1
{R2} is non empty Element of bool the carrier of S1
R1 is non empty directed Element of bool the carrier of S1
{R2} "/\" R1 is non empty Element of bool the carrier of S1
R is non empty directed Element of bool the carrier of S1
R "/\" R1 is non empty directed Element of bool the carrier of S1
"\/" (R1,S1) is Element of the carrier of S1
R2 "/\" ("\/" (R1,S1)) is Element of the carrier of S1
"\/" (({R2} "/\" R1),S1) is Element of the carrier of S1

the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty reflexive non void RelStr
the carrier of S2 is non empty set
the InternalRel of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of the carrier of S2
T2 is Element of the carrier of S1
waybelow T2 is non empty directed Element of bool the carrier of S1
bool the carrier of S1 is non empty set
{ b1 where b1 is Element of the carrier of S1 : b1 is_way_below T2 } is set
waybelow T1 is Element of bool the carrier of S2
bool the carrier of S2 is non empty set
{ b1 where b1 is Element of the carrier of S2 : b1 is_way_below T1 } is set
T1 is Element of the carrier of S2
waybelow T1 is Element of bool the carrier of S2
{ b1 where b1 is Element of the carrier of S2 : b1 is_way_below T1 } is set
"\/" ((waybelow T1),S2) is Element of the carrier of S2
T2 is Element of the carrier of S1
waybelow T2 is non empty directed Element of bool the carrier of S1
{ b1 where b1 is Element of the carrier of S1 : b1 is_way_below T2 } is set
"\/" ((waybelow T2),S1) is Element of the carrier of S1
S1 is RelStr
the carrier of S1 is set
bool the carrier of S1 is non empty set
S2 is RelStr
the carrier of S2 is set
bool the carrier of S2 is non empty set
the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
the InternalRel of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of bool the carrier of S1
subrelstr T1 is strict V213(S1) SubRelStr of S1
T2 is Element of bool the carrier of S2
subrelstr T2 is strict V213(S2) SubRelStr of S2
the carrier of () is set
the carrier of () is set
the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is set
bool [: the carrier of (), the carrier of ():] is non empty set
the InternalRel of S2 |_2 the carrier of () is Relation-like set
the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is set
bool [: the carrier of (), the carrier of ():] is non empty set
S1 is non empty RelStr
S2 is non empty RelStr
the carrier of S1 is non empty set
the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
the carrier of S2 is non empty set
the InternalRel of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is SubRelStr of S1
the carrier of T1 is set
the InternalRel of T1 is Relation-like the carrier of T1 -defined the carrier of T1 -valued Element of bool [: the carrier of T1, the carrier of T1:]
[: the carrier of T1, the carrier of T1:] is set
bool [: the carrier of T1, the carrier of T1:] is non empty set
RelStr(# the carrier of T1, the InternalRel of T1 #) is strict RelStr
T2 is SubRelStr of S2
the carrier of T2 is set
the InternalRel of T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued Element of bool [: the carrier of T2, the carrier of T2:]
[: the carrier of T2, the carrier of T2:] is set
bool [: the carrier of T2, the carrier of T2:] is non empty set
RelStr(# the carrier of T2, the InternalRel of T2 #) is strict RelStr
R1 is Element of the carrier of S2
R2 is Element of the carrier of S2
{R1,R2} is non empty Element of bool the carrier of S2
bool the carrier of S2 is non empty set
"/\" ({R1,R2},S2) is Element of the carrier of S2
R is Element of the carrier of S1
C is Element of the carrier of S1
{R,C} is non empty Element of bool the carrier of S1
bool the carrier of S1 is non empty set
"/\" ({R,C},S1) is Element of the carrier of S1
S1 is non empty RelStr
S2 is non empty RelStr
the carrier of S1 is non empty set
the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
the carrier of S2 is non empty set
the InternalRel of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is SubRelStr of S1
the carrier of T1 is set
the InternalRel of T1 is Relation-like the carrier of T1 -defined the carrier of T1 -valued Element of bool [: the carrier of T1, the carrier of T1:]
[: the carrier of T1, the carrier of T1:] is set
bool [: the carrier of T1, the carrier of T1:] is non empty set
RelStr(# the carrier of T1, the InternalRel of T1 #) is strict RelStr
T2 is SubRelStr of S2
the carrier of T2 is set
the InternalRel of T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued Element of bool [: the carrier of T2, the carrier of T2:]
[: the carrier of T2, the carrier of T2:] is set
bool [: the carrier of T2, the carrier of T2:] is non empty set
RelStr(# the carrier of T2, the InternalRel of T2 #) is strict RelStr
R1 is Element of the carrier of S2
R2 is Element of the carrier of S2
{R1,R2} is non empty Element of bool the carrier of S2
bool the carrier of S2 is non empty set
"\/" ({R1,R2},S2) is Element of the carrier of S2
R is Element of the carrier of S1
C is Element of the carrier of S1
{R,C} is non empty Element of bool the carrier of S1
bool the carrier of S1 is non empty set
"\/" ({R,C},S1) is Element of the carrier of S1
S1 is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty reflexive non void RelStr
the carrier of S2 is non empty set
bool the carrier of S2 is non empty set
the InternalRel of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of bool the carrier of S1
T2 is Element of bool the carrier of S2
R1 is non empty directed Element of bool the carrier of S2
"\/" (R1,S2) is Element of the carrier of S2
R2 is non empty directed Element of bool the carrier of S1
"\/" (R2,S1) is Element of the carrier of S1
R is Element of the carrier of S1
C is Element of the carrier of S2
BT is Element of the carrier of S2
S1 is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
RelStr(# the carrier of S1, the InternalRel of S1 #) is strict RelStr
S2 is non empty reflexive non void RelStr
the carrier of S2 is non empty set
bool the carrier of S2 is non empty set
the InternalRel of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is non empty set
bool [: the carrier of S2, the carrier of S2:] is non empty set
RelStr(# the carrier of S2, the InternalRel of S2 #) is strict RelStr
T1 is Element of bool the carrier of S1
T2 is Element of bool the carrier of S2
R1 is non empty directed Element of bool the carrier of S2
"\/" (R1,S2) is Element of the carrier of S2
R2 is non empty directed Element of bool the carrier of S1
"\/" (R2,S1) is Element of the carrier of S1
S1 is non empty antisymmetric with_infima RelStr
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
S2 is Element of bool the carrier of S1
T1 is Element of bool the carrier of S1
S2 "/\" T1 is Element of bool the carrier of S1
T2 is upper Element of bool the carrier of S1
S2 /\ T2 is Element of bool the carrier of S1
(S2 "/\" T1) /\ T2 is Element of bool the carrier of S1
R1 is set
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of S1 : ( b1 in S2 & b2 in T1 ) } is set
R2 is Element of the carrier of S1
R is Element of the carrier of S1
C is Element of the carrier of S1
R "/\" C is Element of the carrier of S1
S1 is non empty reflexive non void RelStr
the carrier of S1 is non empty set
id the carrier of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
S1 ~ is non empty strict RelStr
the InternalRel of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
the InternalRel of S1 ~ is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
RelStr(# the carrier of S1,( the InternalRel of S1 ~) #) is strict RelStr
the carrier of (S1 ~) is non empty set
[: the carrier of (S1 ~), the carrier of (S1 ~):] is non empty set
the InternalRel of (S1 ~) is Relation-like the carrier of (S1 ~) -defined the carrier of (S1 ~) -valued Element of bool [: the carrier of (S1 ~), the carrier of (S1 ~):]
bool [: the carrier of (S1 ~), the carrier of (S1 ~):] is non empty set
the InternalRel of S1 /\ the InternalRel of (S1 ~) is Relation-like the carrier of S1 -defined the carrier of (S1 ~) -defined the carrier of S1 -valued the carrier of (S1 ~) -valued Element of bool [: the carrier of (S1 ~), the carrier of (S1 ~):]
S2 is set
T1 is set
T2 is set
[T1,T2] is set
{T1,T2} is non empty set
{T1} is non empty set
{{T1,T2},{T1}} is non empty set
R1 is Element of the carrier of S1
R2 is Element of the carrier of S1

S1 ~ is strict RelStr
the carrier of S1 is set
the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is set
bool [: the carrier of S1, the carrier of S1:] is non empty set
the InternalRel of S1 ~ is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
RelStr(# the carrier of S1,( the InternalRel of S1 ~) #) is strict RelStr
the carrier of (S1 ~) is set
[: the carrier of (S1 ~), the carrier of (S1 ~):] is set
the InternalRel of (S1 ~) is Relation-like the carrier of (S1 ~) -defined the carrier of (S1 ~) -valued Element of bool [: the carrier of (S1 ~), the carrier of (S1 ~):]
bool [: the carrier of (S1 ~), the carrier of (S1 ~):] is non empty set
the InternalRel of S1 /\ the InternalRel of (S1 ~) is Relation-like the carrier of S1 -defined the carrier of (S1 ~) -defined the carrier of S1 -valued the carrier of (S1 ~) -valued Element of bool [: the carrier of (S1 ~), the carrier of (S1 ~):]
id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total Element of bool [: the carrier of S1, the carrier of S1:]
S2 is set
T1 is set
T2 is set
[T1,T2] is set
{T1,T2} is non empty set
{T1} is non empty set
{{T1,T2},{T1}} is non empty set
R2 is Element of the carrier of S1
R1 is Element of the carrier of S1
[R2,R1] is set
{R2,R1} is non empty set
{R2} is non empty set
{{R2,R1},{R2}} is non empty set
S1 is non empty RelStr
[:S1,S1:] is non empty strict RelStr
the carrier of [:S1,S1:] is non empty set
the carrier of S1 is non empty set
[: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
bool [: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
S2 is non empty Relation-like the carrier of [:S1,S1:] -defined the carrier of S1 -valued Function-like total quasi_total Element of bool [: the carrier of [:S1,S1:], the carrier of S1:]
T1 is Element of the carrier of S1
T2 is Element of the carrier of S1
S2 . (T1,T2) is set
[T1,T2] is set
{T1,T2} is non empty set
{T1} is non empty set
{{T1,T2},{T1}} is non empty set
S2 . [T1,T2] is set
[T1,T2] is Element of the carrier of [:S1,S1:]
S2 . [T1,T2] is Element of the carrier of S1

the carrier of [:S1,S1:] is non empty set
bool the carrier of [:S1,S1:] is non empty set
the carrier of S1 is non empty set
inf_op S1 is non empty Relation-like the carrier of [:S1,S1:] -defined the carrier of S1 -valued Function-like total quasi_total V177([:S1,S1:],S1) Element of bool [: the carrier of [:S1,S1:], the carrier of S1:]
[: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
bool [: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
T1 is Element of bool the carrier of [:S1,S1:]
(inf_op S1) .: T1 is Element of bool the carrier of S1
bool the carrier of S1 is non empty set
"/\" (((inf_op S1) .: T1),S1) is Element of the carrier of S1
"/\" (T1,[:S1,S1:]) is Element of the carrier of [:S1,S1:]
(inf_op S1) . ("/\" (T1,[:S1,S1:])) is Element of the carrier of S1
dom (inf_op S1) is Element of bool the carrier of [:S1,S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
T2 is Element of the carrier of S1
[T2,T2] is Element of the carrier of [:S1,S1:]
{T2,T2} is non empty set
{T2} is non empty set
{{T2,T2},{T2}} is non empty set
R1 is Element of the carrier of [:S1,S1:]
(inf_op S1) . R1 is Element of the carrier of S1
R2 is set
R is set
[R2,R] is set
{R2,R} is non empty set
{R2} is non empty set
{{R2,R},{R2}} is non empty set
C is Element of the carrier of S1
BT is Element of the carrier of S1
(S1,(inf_op S1),C,BT) is Element of the carrier of S1
[C,BT] is set
{C,BT} is non empty set
{C} is non empty set
{{C,BT},{C}} is non empty set
(inf_op S1) . [C,BT] is set
C "/\" BT is Element of the carrier of S1
(S1,(inf_op S1),T2,T2) is Element of the carrier of S1
[T2,T2] is set
(inf_op S1) . [T2,T2] is set
T2 "/\" T2 is Element of the carrier of S1

inf_op S1 is non empty Relation-like the carrier of [:S1,S1:] -defined the carrier of S1 -valued Function-like total quasi_total V177([:S1,S1:],S1) Element of bool [: the carrier of [:S1,S1:], the carrier of S1:]
the carrier of [:S1,S1:] is non empty set
the carrier of S1 is non empty set
[: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
bool [: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
bool the carrier of [:S1,S1:] is non empty set
S2 is Element of bool the carrier of [:S1,S1:]
(inf_op S1) .: S2 is Element of bool the carrier of S1
bool the carrier of S1 is non empty set
"/\" (((inf_op S1) .: S2),S1) is Element of the carrier of S1
"/\" (S2,[:S1,S1:]) is Element of the carrier of [:S1,S1:]
(inf_op S1) . ("/\" (S2,[:S1,S1:])) is Element of the carrier of S1

the carrier of [:S1,S1:] is non empty set
bool the carrier of [:S1,S1:] is non empty set
the carrier of S1 is non empty set
sup_op S1 is non empty Relation-like the carrier of [:S1,S1:] -defined the carrier of S1 -valued Function-like total quasi_total V177([:S1,S1:],S1) Element of bool [: the carrier of [:S1,S1:], the carrier of S1:]
[: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
bool [: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
T1 is Element of bool the carrier of [:S1,S1:]
(sup_op S1) .: T1 is Element of bool the carrier of S1
bool the carrier of S1 is non empty set
"\/" (((sup_op S1) .: T1),S1) is Element of the carrier of S1
"\/" (T1,[:S1,S1:]) is Element of the carrier of [:S1,S1:]
(sup_op S1) . ("\/" (T1,[:S1,S1:])) is Element of the carrier of S1
dom (sup_op S1) is Element of bool the carrier of [:S1,S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
T2 is Element of the carrier of S1
[T2,T2] is Element of the carrier of [:S1,S1:]
{T2,T2} is non empty set
{T2} is non empty set
{{T2,T2},{T2}} is non empty set
R1 is Element of the carrier of [:S1,S1:]
(sup_op S1) . R1 is Element of the carrier of S1
R2 is set
R is set
[R2,R] is set
{R2,R} is non empty set
{R2} is non empty set
{{R2,R},{R2}} is non empty set
C is Element of the carrier of S1
BT is Element of the carrier of S1
(S1,(sup_op S1),C,BT) is Element of the carrier of S1
[C,BT] is set
{C,BT} is non empty set
{C} is non empty set
{{C,BT},{C}} is non empty set
(sup_op S1) . [C,BT] is set
C "\/" BT is Element of the carrier of S1
(S1,(sup_op S1),T2,T2) is Element of the carrier of S1
[T2,T2] is set
(sup_op S1) . [T2,T2] is set
T2 "\/" T2 is Element of the carrier of S1

sup_op S1 is non empty Relation-like the carrier of [:S1,S1:] -defined the carrier of S1 -valued Function-like total quasi_total V177([:S1,S1:],S1) Element of bool [: the carrier of [:S1,S1:], the carrier of S1:]
the carrier of [:S1,S1:] is non empty set
the carrier of S1 is non empty set
[: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
bool [: the carrier of [:S1,S1:], the carrier of S1:] is non empty set
bool the carrier of [:S1,S1:] is non empty set
S2 is Element of bool the carrier of [:S1,S1:]
(sup_op S1) .: S2 is Element of bool the carrier of S1
bool the carrier of S1 is non empty set
"\/" (((sup_op S1) .: S2),S1) is Element of the carrier of S1
"\/" (S2,[:S1,S1:]) is Element of the carrier of [:S1,S1:]
(sup_op S1) . ("\/" (S2,[:S1,S1:])) is Element of the carrier of S1

the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
S2 is Element of bool the carrier of S1

T1 is Element of the carrier of S1
T2 is Element of the carrier of S1
T1 "/\" T2 is Element of the carrier of S1
the carrier of () is set
{T1,T2} is non empty Element of bool the carrier of S1
"/\" ({T1,T2},S1) is Element of the carrier of S1

the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
S2 is Element of bool the carrier of S1

T1 is Element of the carrier of S1
T2 is Element of the carrier of S1
T1 "\/" T2 is Element of the carrier of S1
the carrier of () is set
{T1,T2} is non empty Element of bool the carrier of S1
"\/" ({T1,T2},S1) is Element of the carrier of S1
S1 is transitive RelStr
the carrier of S1 is set
bool the carrier of S1 is non empty set
T1 is Element of bool the carrier of S1
uparrow T1 is Element of bool the carrier of S1
S2 is Element of bool the carrier of S1
uparrow S2 is Element of bool the carrier of S1
T2 is set
R1 is Element of the carrier of S1
R2 is Element of the carrier of S1
R is Element of the carrier of S1
C is Element of the carrier of S1
S1 is transitive RelStr
the carrier of S1 is set
bool the carrier of S1 is non empty set
S2 is Element of bool the carrier of S1
T1 is Element of bool the carrier of S1
downarrow T1 is Element of bool the carrier of S1
downarrow S2 is Element of bool the carrier of S1
T2 is set
R1 is Element of the carrier of S1
R2 is Element of the carrier of S1
R is Element of the carrier of S1
C is Element of the carrier of S1
S1 is non empty reflexive non void RelStr
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
S2 is Element of the carrier of S1
uparrow S2 is non empty filtered Element of bool the carrier of S1
{S2} is non empty Element of bool the carrier of S1
uparrow {S2} is non empty Element of bool the carrier of S1
T1 is Element of bool the carrier of S1
uparrow T1 is Element of bool the carrier of S1
T2 is set
R1 is Element of the carrier of S1
S1 is non empty reflexive non void RelStr
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
S2 is Element of the carrier of S1
downarrow S2 is non empty directed Element of bool the carrier of S1
{S2} is non empty Element of bool the carrier of S1
downarrow {S2} is non empty Element of bool the carrier of S1
T1 is Element of bool the carrier of S1
downarrow T1 is Element of bool the carrier of S1
T2 is set
R1 is Element of the carrier of S1
S1 is TopStruct
the carrier of S1 is set
bool the carrier of S1 is non empty set
bool (bool the carrier of S1) is non empty set
the topology of S1 is Element of bool (bool the carrier of S1)
TopStruct(# the carrier of S1, the topology of S1 #) is strict TopStruct
S2 is TopStruct
the carrier of S2 is set
the topology of S2 is Element of bool (bool the carrier of S2)
bool the carrier of S2 is non empty set
bool (bool the carrier of S2) is non empty set
TopStruct(# the carrier of S2, the topology of S2 #) is strict TopStruct
T1 is open quasi_basis Element of bool (bool the carrier of S1)
UniCl T1 is Element of bool (bool the carrier of S1)
S1 is TopStruct
the carrier of S1 is set
bool the carrier of S1 is non empty set
bool (bool the carrier of S1) is non empty set
the topology of S1 is Element of bool (bool the carrier of S1)
TopStruct(# the carrier of S1, the topology of S1 #) is strict TopStruct
S2 is TopStruct
the carrier of S2 is set
the topology of S2 is Element of bool (bool the carrier of S2)
bool the carrier of S2 is non empty set
bool (bool the carrier of S2) is non empty set
TopStruct(# the carrier of S2, the topology of S2 #) is strict TopStruct
T1 is open quasi_prebasis Element of bool (bool the carrier of S1)
FinMeetCl T1 is Element of bool (bool the carrier of S1)
T2 is open quasi_basis Element of bool (bool the carrier of S1)
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
bool (bool the carrier of S1) is non empty set
S2 is open quasi_basis Element of bool (bool the carrier of S1)
UniCl S2 is Element of bool (bool the carrier of S1)
the topology of S1 is non empty Element of bool (bool the carrier of S1)
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
bool (bool the carrier of S1) is non empty set
S2 is open quasi_basis Element of bool (bool the carrier of S1)
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
bool (bool the carrier of S1) is non empty set
S2 is Element of the carrier of S1
T1 is open V225(S1,S2) Element of bool (bool the carrier of S1)
[#] S1 is non empty non proper open closed dense non boundary Element of bool the carrier of S1
T2 is Element of bool the carrier of S1
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
S2 is Element of the carrier of S1
bool the carrier of S1 is non empty set
bool (bool the carrier of S1) is non empty set
T1 is open V225(S1,S2) Element of bool (bool the carrier of S1)

the carrier of S1 is set

the carrier of T1 is set
[: the carrier of S1, the carrier of T1:] is set
bool [: the carrier of S1, the carrier of T1:] is non empty set

the carrier of S2 is set

the carrier of T2 is set
[: the carrier of S2, the carrier of T2:] is set
bool [: the carrier of S2, the carrier of T2:] is non empty set
the topology of S1 is non empty Element of bool (bool the carrier of S1)
bool the carrier of S1 is non empty set
bool (bool the carrier of S1) is non empty set
TopStruct(# the carrier of S1, the topology of S1 #) is strict TopSpace-like TopStruct
the topology of S2 is non empty Element of bool (bool the carrier of S2)
bool the carrier of S2 is non empty set
bool (bool the carrier of S2) is non empty set
TopStruct(# the carrier of S2, the topology of S2 #) is strict TopSpace-like TopStruct
the topology of T1 is non empty Element of bool (bool the carrier of T1)
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
TopStruct(# the carrier of T1, the topology of T1 #) is strict TopSpace-like TopStruct
the topology of T2 is non empty Element of bool (bool the carrier of T2)
bool the carrier of T2 is non empty set
bool (bool the carrier of T2) is non empty set
TopStruct(# the carrier of T2, the topology of T2 #) is strict TopSpace-like TopStruct
R1 is Relation-like the carrier of S1 -defined the carrier of T1 -valued Function-like quasi_total Element of bool [: the carrier of S1, the carrier of T1:]
R2 is Relation-like the carrier of S2 -defined the carrier of T2 -valued Function-like quasi_total Element of bool [: the carrier of S2, the carrier of T2:]
R is Element of bool the carrier of T2
C is Element of bool the carrier of T1
R1 " C is Element of bool the carrier of S1
R2 " R is Element of bool the carrier of S2
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
id the carrier of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is non empty set
bool [: the carrier of S1, the carrier of S1:] is non empty set
[:S1,S1:] is non empty strict TopSpace-like TopStruct
the carrier of [:S1,S1:] is non empty set
pr1 ( the carrier of S1, the carrier of S1) is non empty Relation-like [: the carrier of S1, the carrier of S1:] -defined the carrier of S1 -valued Function-like total quasi_total Element of bool [:[: the carrier of S1, the carrier of S1:], the carrier of S1:]
[:[: the carrier of S1, the carrier of S1:], the carrier of S1:] is non empty set
bool [:[: the carrier of S1, the carrier of S1:], the carrier of S1:] is non empty set
pr2 ( the carrier of S1, the carrier of S1) is non empty Relation-like [: the carrier of S1, the carrier of S1:] -defined the carrier of S1 -valued Function-like total quasi_total Element of bool [:[: the carrier of S1, the carrier of S1:], the carrier of S1:]
{ b1 where b1 is Element of the carrier of [:S1,S1:] : (pr1 ( the carrier of S1, the carrier of S1)) . b1 = (pr2 ( the carrier of S1, the carrier of S1)) . b1 } is set
T2 is set
R1 is set
R2 is set
[R1,R2] is set
{R1,R2} is non empty set
{R1} is non empty set
{{R1,R2},{R1}} is non empty set
(pr1 ( the carrier of S1, the carrier of S1)) . (R1,R2) is set
(pr1 ( the carrier of S1, the carrier of S1)) . [R1,R2] is set
(pr2 ( the carrier of S1, the carrier of S1)) . (R1,R2) is set
(pr2 ( the carrier of S1, the carrier of S1)) . [R1,R2] is set
T2 is set
R1 is Element of the carrier of [:S1,S1:]
(pr1 ( the carrier of S1, the carrier of S1)) . R1 is set
(pr2 ( the carrier of S1, the carrier of S1)) . R1 is set
R2 is set
R is set
[R2,R] is set
{R2,R} is non empty set
{R2} is non empty set
{{R2,R},{R2}} is non empty set
(pr1 ( the carrier of S1, the carrier of S1)) . (R2,R) is set
(pr1 ( the carrier of S1, the carrier of S1)) . [R2,R] is set
(pr2 ( the carrier of S1, the carrier of S1)) . (R2,R) is set
(pr2 ( the carrier of S1, the carrier of S1)) . [R2,R] is set
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
delta the carrier of S1 is non empty Relation-like the carrier of S1 -defined [: the carrier of S1, the carrier of S1:] -valued Function-like total quasi_total Element of bool [: the carrier of S1,[: the carrier of S1, the carrier of S1:]:]
[: the carrier of S1, the carrier of S1:] is non empty set
[: the carrier of S1,[: the carrier of S1, the carrier of S1:]:] is non empty set
bool [: the carrier of S1,[: the carrier of S1, the carrier of S1:]:] is non empty set
[:S1,S1:] is non empty strict TopSpace-like TopStruct
the carrier of [:S1,S1:] is non empty set
[: the carrier of S1, the carrier of [:S1,S1:]:] is non empty set
bool [: the carrier of S1, the carrier of [:S1,S1:]:] is non empty set
S2 is non empty Relation-like the carrier of S1 -defined the carrier of [:S1,S1:] -valued Function-like total quasi_total Element of bool [: the carrier of S1, the carrier of [:S1,S1:]:]
T1 is Element of the carrier of S1
S2 . T1 is Element of the carrier of [:S1,S1:]
T2 is a_neighborhood of S2 . T1
bool the carrier of [:S1,S1:] is non empty set
bool (bool the carrier of [:S1,S1:]) is non empty set
Int T2 is open Element of bool the carrier of [:S1,S1:]
bool the carrier of S1 is non empty set
R1 is Element of bool (bool the carrier of [:S1,S1:])
union R1 is Element of bool the carrier of [:S1,S1:]
R2 is set
R is Element of bool the carrier of S1
C is Element of bool the carrier of S1
[:R,C:] is Element of bool the carrier of [:S1,S1:]
[T1,T1] is Element of the carrier of [:S1,S1:]
{T1,T1} is non empty set
{T1} is non empty set
{{T1,T1},{T1}} is non empty set
R /\ C is Element of bool the carrier of S1
Int (R /\ C) is open Element of bool the carrier of S1
BT is a_neighborhood of T1
S2 .: BT is Element of bool the carrier of [:S1,S1:]
BS is set
dom S2 is Element of bool the carrier of S1
Bpr is set
S2 . Bpr is set
[Bpr,Bpr] is set
{Bpr,Bpr} is non empty set
{Bpr} is non empty set
{{Bpr,Bpr},{Bpr}} is non empty set
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
S2 is non empty TopSpace-like TopStruct
the carrier of S2 is non empty set
pr1 ( the carrier of S1, the carrier of S2) is non empty Relation-like [: the carrier of S1, the carrier of S2:] -defined the carrier of S1 -valued Function-like total quasi_total Element of bool [:[: the carrier of S1, the carrier of S2:], the carrier of S1:]
[: the carrier of S1, the carrier of S2:] is non empty set
[:[: the carrier of S1, the carrier of S2:], the carrier of S1:] is non empty set
bool [:[: the carrier of S1, the carrier of S2:], the carrier of S1:] is non empty set
[:S1,S2:] is non empty strict TopSpace-like TopStruct
the carrier of [:S1,S2:] is non empty set
[: the carrier of [:S1,S2:], the carrier of S1:] is non empty set
bool [: the carrier of [:S1,S2:], the carrier of S1:] is non empty set
R1 is non empty Relation-like the carrier of [:S1,S2:] -defined the carrier of S1 -valued Function-like total quasi_total Element of bool [: the carrier of [:S1,S2:], the carrier of S1:]
R2 is Element of the carrier of [:S1,S2:]
R1 . R2 is Element of the carrier of S1
R is a_neighborhood of R1 . R2
Int R is open Element of bool the carrier of S1
bool the carrier of S1 is non empty set
[#] S2 is non empty non proper open closed dense non boundary Element of bool the carrier of S2
bool the carrier of S2 is non empty set
[:(Int R),([#] S2):] is Element of bool the carrier of [:S1,S2:]
bool the carrier of [:S1,S2:] is non empty set
Int [:(Int R),([#] S2):] is open Element of bool the carrier of [:S1,S2:]
Int (Int R) is open Element of bool the carrier of S1
Int ([#] S2) is open Element of bool the carrier of S2
[:(Int (Int R)),(Int ([#] S2)):] is Element of bool the carrier of [:S1,S2:]
BT is set
BS is set
[BT,BS] is set
{BT,BS} is non empty set
{BT} is non empty set
{{BT,BS},{BT}} is non empty set
R1 . (BT,BS) is set
R1 . [BT,BS] is set
Bpr is a_neighborhood of R2
R1 .: Bpr is Element of bool the carrier of S1
c is non empty Element of bool the carrier of S1
[:c,([#] S2):] is non empty Element of bool the carrier of [:S1,S2:]
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
S2 is non empty TopSpace-like TopStruct
the carrier of S2 is non empty set
pr2 ( the carrier of S1, the carrier of S2) is non empty Relation-like [: the carrier of S1, the carrier of S2:] -defined the carrier of S2 -valued Function-like total quasi_total Element of bool [:[: the carrier of S1, the carrier of S2:], the carrier of S2:]
[: the carrier of S1, the carrier of S2:] is non empty set
[:[: the carrier of S1, the carrier of S2:], the carrier of S2:] is non empty set
bool [:[: the carrier of S1, the carrier of S2:], the carrier of S2:] is non empty set
[:S1,S2:] is non empty strict TopSpace-like TopStruct
the carrier of [:S1,S2:] is non empty set
[: the carrier of [:S1,S2:], the carrier of S2:] is non empty set
bool [: the carrier of [:S1,S2:], the carrier of S2:] is non empty set
R1 is non empty Relation-like the carrier of [:S1,S2:] -defined the carrier of S2 -valued Function-like total quasi_total Element of bool [: the carrier of [:S1,S2:], the carrier of S2:]
R2 is Element of the carrier of [:S1,S2:]
R1 . R2 is Element of the carrier of S2
R is a_neighborhood of R1 . R2
[#] S1 is non empty non proper open closed dense non boundary Element of bool the carrier of S1
bool the carrier of S1 is non empty set
Int R is open Element of bool the carrier of S2
bool the carrier of S2 is non empty set
[:([#] S1),(Int R):] is Element of bool the carrier of [:S1,S2:]
bool the carrier of [:S1,S2:] is non empty set
Int [:([#] S1),(Int R):] is open Element of bool the carrier of [:S1,S2:]
Int ([#] S1) is open Element of bool the carrier of S1
Int (Int R) is open Element of bool the carrier of S2
[:(Int ([#] S1)),(Int (Int R)):] is Element of bool the carrier of [:S1,S2:]
BT is set
BS is set
[BT,BS] is set
{BT,BS} is non empty set
{BT} is non empty set
{{BT,BS},{BT}} is non empty set
R1 . (BT,BS) is set
R1 . [BT,BS] is set
Bpr is a_neighborhood of R2
R1 .: Bpr is Element of bool the carrier of S2
c is non empty Element of bool the carrier of S2
[:([#] S1),c:] is non empty Element of bool the carrier of [:S1,S2:]
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
S2 is non empty TopSpace-like TopStruct
the carrier of S2 is non empty set
[: the carrier of S1, the carrier of S2:] is non empty set
bool [: the carrier of S1, the carrier of S2:] is non empty set
T1 is non empty TopSpace-like TopStruct
the carrier of T1 is non empty set
[: the carrier of S1, the carrier of T1:] is non empty set
bool [: the carrier of S1, the carrier of T1:] is non empty set
[:S2,T1:] is non empty strict TopSpace-like TopStruct
the carrier of [:S2,T1:] is non empty set
[: the carrier of S1, the carrier of [:S2,T1:]:] is non empty set
bool [: the carrier of S1, the carrier of [:S2,T1:]:] is non empty set
T2 is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total quasi_total continuous Element of bool [: the carrier of S1, the carrier of S2:]
R1 is non empty Relation-like the carrier of S1 -defined the carrier of T1 -valued Function-like total quasi_total continuous Element of bool [: the carrier of S1, the carrier of T1:]
<:T2,R1:> is non empty Relation-like the carrier of S1 -defined [: the carrier of S2, the carrier of T1:] -valued Function-like total quasi_total Element of bool [: the carrier of S1,[: the carrier of S2, the carrier of T1:]:]
[: the carrier of S2, the carrier of T1:] is non empty set
[: the carrier of S1,[: the carrier of S2, the carrier of T1:]:] is non empty set
bool [: the carrier of S1,[: the carrier of S2, the carrier of T1:]:] is non empty set
[: the carrier of S1, the carrier of S1:] is non empty set
[:S1,S1:] is non empty strict TopSpace-like TopStruct
the carrier of [:S1,S1:] is non empty set
delta the carrier of S1 is non empty Relation-like the carrier of S1 -defined [: the carrier of S1, the carrier of S1:] -valued Function-like total quasi_total Element of bool [: the carrier of S1,[: the carrier of S1, the carrier of S1:]:]
[: the carrier of S1,[: the carrier of S1, the carrier of S1:]:] is non empty set
bool [: the carrier of S1,[: the carrier of S1, the carrier of S1:]:] is non empty set
[:T2,R1:] is non empty Relation-like the carrier of [:S1,S1:] -defined the carrier of [:S2,T1:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:S1,S1:], the carrier of [:S2,T1:]:]
[: the carrier of [:S1,S1:], the carrier of [:S2,T1:]:] is non empty set
bool [: the carrier of [:S1,S1:], the carrier of [:S2,T1:]:] is non empty set
[:T2,R1:] * (delta the carrier of S1) is Relation-like the carrier of S1 -defined the carrier of [:S2,T1:] -valued Function-like Element of bool [: the carrier of S1, the carrier of [:S2,T1:]:]
[: the carrier of S1, the carrier of [:S1,S1:]:] is non empty set
bool [: the carrier of S1, the carrier of [:S1,S1:]:] is non empty set
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
S2 is non empty TopSpace-like TopStruct
the carrier of S2 is non empty set
[: the carrier of S1, the carrier of S2:] is non empty set
pr2 ( the carrier of S1, the carrier of S2) is non empty Relation-like [: the carrier of S1, the carrier of S2:] -defined the carrier of S2 -valued Function-like total quasi_total Element of bool [:[: the carrier of S1, the carrier of S2:], the carrier of S2:]
[:[: the carrier of S1, the carrier of S2:], the carrier of S2:] is non empty set
bool [:[: the carrier of S1, the carrier of S2:], the carrier of S2:] is non empty set
pr1 ( the carrier of S1, the carrier of S2) is non empty Relation-like [: the carrier of S1, the carrier of S2:] -defined the carrier of S1 -valued Function-like total quasi_total Element of bool [:[: the carrier of S1, the carrier of S2:], the carrier of S1:]
[:[: the carrier of S1, the carrier of S2:], the carrier of S1:] is non empty set
bool [:[: the carrier of S1, the carrier of S2:], the carrier