:: YELLOW12 semantic presentation

K259() is non empty strict TopSpace-like T_0 T_1 T_2 V73() normal T_3 T_4 V114() locally-compact compact SubSpace of K257()
K257() is TopSpace-like TopStruct
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
{} is empty set
the empty set is empty set
1 is non empty set
{{},1} is non empty set
K219() is non empty strict TopSpace-like T_0 T_1 T_2 V73() normal T_3 T_4 V114() locally-compact compact TopStruct
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
union {} is 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
S1 is non empty reflexive transitive antisymmetric with_infima 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 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
S1 is non empty reflexive transitive antisymmetric with_suprema 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 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
S1 is non empty reflexive transitive antisymmetric with_infima 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 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
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of S1 : ( b₁ in T1 & b₂ in T2 ) } is set
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of S2 : ( b₁ in R1 & b₂ 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 transitive antisymmetric with_suprema 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 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
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of S1 : ( b₁ in T1 & b₂ in T2 ) } is set
{ (b₁ "\/" b₂) where b₁, b₂ is Element of the carrier of S2 : ( b₁ in R1 & b₂ 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
{ b₁ where b₁ is Element of the carrier of S1 : b₁ is_way_below T1 } is set
wayabove T1 is Element of bool the carrier of S1
{ b₁ where b₁ is Element of the carrier of S1 : T1 is_way_below b₁ } 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
{ b₁ where b₁ is Element of the carrier of S2 : b₁ is_way_below T2 } is set
wayabove T2 is Element of bool the carrier of S2
{ b₁ where b₁ is Element of the carrier of S2 : T2 is_way_below b₁ } 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
S1 is non empty reflexive transitive antisymmetric with_infima up-complete non void satisfying_MC meet-continuous 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
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
S1 is non empty reflexive antisymmetric satisfying_axiom_of_approximation continuous 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 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
{ b₁ where b₁ is Element of the carrier of S1 : b₁ 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
{ b₁ where b₁ is Element of the carrier of S2 : b₁ is_way_below T1 } is set
T1 is Element of the carrier of S2
waybelow T1 is Element of bool the carrier of S2
{ b₁ where b₁ is Element of the carrier of S2 : b₁ 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
{ b₁ where b₁ is Element of the carrier of S1 : b₁ 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 (subrelstr T1) is set
the carrier of (subrelstr T2) is set
the InternalRel of (subrelstr T1) is Relation-like the carrier of (subrelstr T1) -defined the carrier of (subrelstr T1) -valued Element of bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):]
[: the carrier of (subrelstr T1), the carrier of (subrelstr T1):] is set
bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):] is non empty set
the InternalRel of S2 |_2 the carrier of (subrelstr T2) is Relation-like set
the InternalRel of (subrelstr T2) is Relation-like the carrier of (subrelstr T2) -defined the carrier of (subrelstr T2) -valued Element of bool [: the carrier of (subrelstr T2), the carrier of (subrelstr T2):]
[: the carrier of (subrelstr T2), the carrier of (subrelstr T2):] is set
bool [: the carrier of (subrelstr T2), the carrier of (subrelstr T2):] 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
{ (b₁ "/\" b₂) where b₁, b₂ is Element of the carrier of S1 : ( b₁ in S2 & b₂ 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 antisymmetric RelStr
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
S1 is non empty reflexive transitive antisymmetric with_infima upper-bounded non void RelStr
[:S1,S1:] is non empty strict reflexive transitive antisymmetric with_infima non void RelStr
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
S1 is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V212() up-complete /\-complete non void RelStr
[:S1,S1:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V212() up-complete /\-complete non void RelStr
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
S1 is non empty reflexive transitive antisymmetric with_suprema lower-bounded non void RelStr
[:S1,S1:] is non empty strict reflexive transitive antisymmetric with_suprema non void RelStr
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
S1 is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V212() up-complete /\-complete non void RelStr
[:S1,S1:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V212() up-complete /\-complete non void RelStr
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
S1 is non empty reflexive transitive antisymmetric with_infima non void 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
subrelstr S2 is strict reflexive transitive antisymmetric V213(S1) SubRelStr 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 (subrelstr S2) 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 non empty reflexive transitive antisymmetric with_suprema non void 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
subrelstr S2 is strict reflexive transitive antisymmetric V213(S1) SubRelStr 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 (subrelstr S2) 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)
S1 is TopSpace-like TopStruct
the carrier of S1 is set
T1 is TopSpace-like TopStruct
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
S2 is TopSpace-like TopStruct
the carrier of S2 is set
T2 is TopSpace-like TopStruct
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:]
{ b₁ where b₁ is Element of the carrier of [:S1,S1:] : (pr1 ( the carrier of S1, the carrier of S1)) . b₁ = (pr2 ( the carrier of S1, the carrier of S1)) . b₁ } 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 of S1:] is non empty set
<:(pr2 ( the carrier of S1, the carrier of S2)),(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 S2, the carrier of S1:] -valued Function-like one-to-one 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 S1:] is non empty set
[:[: the carrier of S1, the carrier of S2:],[: the carrier of S2, the carrier of S1:]:] is non empty set
bool [:[: the carrier of S1, the carrier of S2:],[: 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
[:S2,S1:] is non empty strict TopSpace-like TopStruct
the carrier of [:S2,S1:] is non empty set
[: the carrier of [:S1,S2:], the carrier of [:S2,S1:]:] is non empty set
bool [: the carrier of [:S1,S2:], the carrier of [:S2,S1:]:] 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
[: 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
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
S2 is non empty TopSpace-like TopStruct
[:S1,S2:] is non empty strict TopSpace-like TopStruct
the carrier of [:S1,S2:] is non empty set
[:S2,S1:] is non empty strict TopSpace-like TopStruct
the carrier of [:S2,S1:] is non empty set
[: the carrier of [:S1,S2:], the carrier of [:S2,S1:]:] is non empty set
bool [: the carrier of [:S1,S2:], the carrier of [:S2,S1:]:] is non empty set
the carrier of S2 is non empty set
[: the carrier of S1, the carrier of S2:] is non empty set
[: the carrier of S2, the carrier of S1:] 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 of S1:] is non empty set
<:(pr2 ( the carrier of S1, the carrier of S2)),(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 S2, the carrier of S1:] -valued Function-like one-to-one 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 S1, the carrier of S2:],[: the carrier of S2, the carrier of S1:]:] is non empty set
bool [:[: the carrier of S1, the carrier of S2:],[: the carrier of S2, the carrier of S1:]:] is non empty set
T1 is non empty Relation-like the carrier of [:S1,S2:] -defined the carrier of [:S2,S1:] -valued Function-like total quasi_total Element of bool [: the carrier of [:S1,S2:], the carrier of [:S2,S1:]:]
dom T1 is Element of bool the carrier of [:S1,S2:]
bool the carrier of [:S1,S2:] is non empty set
[#] [:S1,S2:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:S1,S2:]
rng T1 is Element of bool the carrier of [:S2,S1:]
bool the carrier of [:S2,S1:] is non empty set
[#] [:S2,S1:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:S2,S1:]
T1 " is non empty Relation-like the carrier of [:S2,S1:] -defined the carrier of [:S1,S2:] -valued Function-like total quasi_total Element of bool [: the carrier of [:S2,S1:], the carrier of [:S1,S2:]:]
[: the carrier of [:S2,S1:], the carrier of [:S1,S2:]:] is non empty set
bool [: the carrier of [:S2,S1:], the carrier of [:S1,S2:]:] is non empty set
T1 " is Relation-like Function-like set
pr2 ( the carrier of S2, the carrier of S1) is non empty Relation-like [: the carrier of S2, the carrier of S1:] -defined the carrier of S1 -valued Function-like total quasi_total Element of bool [:[: the carrier of S2, the carrier of S1:], the carrier of S1:]
[:[: the carrier of S2, the carrier of S1:], the carrier of S1:] is non empty set
bool [:[: the carrier of S2, the carrier of S1:], the carrier of S1:] is non empty set
pr1 ( the carrier of S2, the carrier of S1) is non empty Relation-like [: the carrier of S2, the carrier of S1:] -defined the carrier of S2 -valued Function-like total quasi_total Element of bool [:[: the carrier of S2, the carrier of S1:], the carrier of S2:]
[:[: the carrier of S2, the carrier of S1:], the carrier of S2:] is non empty set
bool [:[: the carrier of S2, the carrier of S1:], the carrier of S2:] is non empty set
<:(pr2 ( the carrier of S2, the carrier of S1)),(pr1 ( the carrier of S2, the carrier of S1)):> is non empty Relation-like [: the carrier of S2, the carrier of S1:] -defined [: the carrier of S1, the carrier of S2:] -valued Function-like one-to-one total quasi_total Element of bool [:[: the carrier of S2, the carrier of S1:],[: the carrier of S1, the carrier of S2:]:]
[:[: the carrier of S2, the carrier of S1:],[: the carrier of S1, the carrier of S2:]:] is non empty set
bool [:[: the carrier of S2, the carrier of S1:],[: the carrier of S1, the carrier of S2:]:] is non empty set
S1 is non empty TopSpace-like TopStruct
S2 is non empty TopSpace-like TopStruct
[:S1,S2:] is non empty strict TopSpace-like TopStruct
[:S2,S1:] is non empty strict TopSpace-like TopStruct
the carrier of [:S1,S2:] is non empty set
the carrier of [:S2,S1:] is non empty set
[: the carrier of [:S1,S2:], the carrier of [:S2,S1:]:] is non empty set
bool [: the carrier of [:S1,S2:], the carrier of [:S2,S1:]:] is non empty set
the carrier of S1 is non empty set
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 of S1:] is non empty set
<:(pr2 ( the carrier of S1, the carrier of S2)),(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 S2, the carrier of S1:] -valued Function-like one-to-one 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 S1:] is non empty set
[:[: the carrier of S1, the carrier of S2:],[: the carrier of S2, the carrier of S1:]:] is non empty set
bool [:[: the carrier of S1, the carrier of S2:],[: the carrier of S2, the carrier of S1:]:] is non empty set
T1 is non empty Relation-like the carrier of [:S1,S2:] -defined the carrier of [:S2,S1:] -valued Function-like total quasi_total Element of bool [: the carrier of [:S1,S2:], the carrier of [:S2,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
S2 is non empty TopSpace-like T_0 T_1 T_2 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 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:]
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:]
{ b₁ where b₁ is Element of the carrier of S1 : not T1 . b₁ = T2 . b₁ } is set
{ b₁ where b₁ is Element of the carrier of S1 : T1 . b₁ = T2 . b₁ } is set
R1 is set
R2 is Element of the carrier of S1
T1 . R2 is Element of the carrier of S2
T2 . R2 is Element of the carrier of S2
[#] 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
R2 is Element of bool the carrier of S1
R is set
C is Element of the carrier of S1
T1 . C is Element of the carrier of S2
T2 . C is Element of the carrier of S2
BT is Element of bool the carrier of S2
BS is Element of bool the carrier of S2
dom T2 is Element of bool the carrier of S1
[R,(T2 . C)] is set
{R,(T2 . C)} is non empty set
{R} is non empty set
{{R,(T2 . C)},{R}} is non empty set
T2 " BS is Element of bool the carrier of S1
T1 " BT is Element of bool the carrier of S1
(T1 " BT) /\ (T2 " BS) is Element of bool the carrier of S1
Bpr is Element of bool the carrier of S1
c is set
a is set
[c,a] is set
{c,a} is non empty set
{c} is non empty set
{{c,a},{c}} is non empty set
b is set
[c,b] is set
{c,b} is non empty set
{{c,b},{c}} is non empty set
T2 . c is set
T1 . c is set
dom T1 is Element of bool the carrier of S1
[R,(T1 . C)] is set
{R,(T1 . C)} is non empty set
{{R,(T1 . C)},{R}} is non empty set
C is Element of bool the carrier of S1
R1 is Element of bool the carrier of S1
R2 is Element of bool the carrier of S1
R2 ` is Element of bool the carrier of S1
the carrier of S1 \ R2 is set
R is set
T1 . R is set
T2 . R is set
R is set
C is Element of the carrier of S1
T1 . C is Element of the carrier of S2
T2 . C is Element of the carrier of S2
BT is Element of the carrier of S1
T1 . BT is Element of the carrier of S2
T2 . BT is Element of the carrier of S2
S1 is non empty TopSpace-like TopStruct
[:S1,S1:] is non empty strict TopSpace-like TopStruct
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
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
[: 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
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:]
R1 is Element of bool the carrier of [:S1,S1:]
S2 is non empty Relation-like the carrier of [:S1,S1:] -defined the carrier of S1 -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:S1,S1:], the carrier of S1:]
T1 is non empty Relation-like the carrier of [:S1,S1:] -defined the carrier of S1 -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:S1,S1:], the carrier of S1:]
{ b₁ where b₁ is Element of the carrier of [:S1,S1:] : S2 . b₁ = T1 . b₁ } is set
[#] [:S1,S1:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:S1,S1:]
[#] 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
[:([#] S1),([#] S1):] is non empty Element of bool the carrier of [:S1,S1:]
T2 is Element of bool the carrier of [:S1,S1:]
[:([#] S1),([#] S1):] \ T2 is Element of bool the carrier of [:S1,S1:]
bool (bool the carrier of [:S1,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 Element of the carrier of S1
R is Element of the carrier of S1
[R2,R] is Element of the carrier of [:S1,S1:]
{R2,R} is non empty set
{R2} is non empty set
{{R2,R},{R2}} is non empty set
id ([#] S1) is non empty Relation-like [#] S1 -defined [#] S1 -valued total quasi_total Element of bool [:([#] S1),([#] S1):]
[:([#] S1),([#] S1):] is non empty set
bool [:([#] S1),([#] S1):] is non empty set
C is set
BT is Element of bool the carrier of S1
BS is Element of bool the carrier of S1
[:BT,BS:] is Element of bool the carrier of [:S1,S1:]
BT /\ BS is Element of bool the carrier of S1
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 TopStruct
S2 is TopStruct
the TopSpace-like Refinement of S1,S2 is TopSpace-like Refinement of S1,S2
the carrier of the TopSpace-like Refinement of S1,S2 is set
the topology of the TopSpace-like Refinement of S1,S2 is non empty Element of bool (bool the carrier of the TopSpace-like Refinement of S1,S2)
bool the carrier of the TopSpace-like Refinement of S1,S2 is non empty set
bool (bool the carrier of the TopSpace-like Refinement of S1,S2) is non empty set
TopStruct(# the carrier of the TopSpace-like Refinement of S1,S2, the topology of the TopSpace-like Refinement of S1,S2 #) is strict TopSpace-like TopStruct
the topology of S1 is Element of bool (bool the carrier of S1)
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 S2 is Element of bool (bool the carrier of S2)
the carrier of S2 is set
bool the carrier of S2 is non empty set
bool (bool the carrier of S2) is non empty set
the topology of S1 \/ the topology of S2 is set
the carrier of TopStruct(# the carrier of the TopSpace-like Refinement of S1,S2, the topology of the TopSpace-like Refinement of S1,S2 #) is set
the carrier of S1 \/ the carrier of S2 is set
bool the carrier of TopStruct(# the carrier of the TopSpace-like Refinement of S1,S2, the topology of the TopSpace-like Refinement of S1,S2 #) is non empty set
bool (bool the carrier of TopStruct(# the carrier of the TopSpace-like Refinement of S1,S2, the topology of the TopSpace-like Refinement of S1,S2 #)) is non empty set
R1 is TopSpace-like Refinement of S1,S2
S1 is non empty TopStruct
S2 is TopStruct
the non empty strict TopSpace-like Refinement of S1,S2 is non empty strict TopSpace-like Refinement of S1,S2
the non empty strict TopSpace-like Refinement of S2,S1 is non empty strict TopSpace-like Refinement of S2,S1
S1 is TopStruct
S2 is TopStruct
T1 is TopStruct
the carrier of S1 is set
the topology of S1 is 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 TopStruct
the topology of S2 is Element of bool (bool the carrier of S2)
the carrier of S2 is set
bool the carrier of S2 is non empty set
bool (bool the carrier of S2) is non empty set
the topology of T1 is Element of bool (bool the carrier of T1)
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
the topology of S2 \/ the topology of T1 is set
T2 is TopSpace-like TopStruct
the carrier of T2 is set
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
the carrier of TopStruct(# the carrier of T2, the topology of T2 #) is set
bool the carrier of TopStruct(# the carrier of T2, the topology of T2 #) is non empty set
bool (bool the carrier of TopStruct(# the carrier of T2, the topology of T2 #)) is non empty set
the carrier of S2 \/ the carrier of T1 is set
the carrier of TopStruct(# the carrier of S1, the topology of S1 #) is set
bool the carrier of TopStruct(# the carrier of S1, the topology of S1 #) is non empty set
bool (bool the carrier of TopStruct(# the carrier of S1, the topology of S1 #)) is non empty set
T2 is TopSpace-like TopStruct
the carrier of T2 is set
bool the carrier of T2 is non empty set
bool (bool the carrier of T2) is non empty set
S1 is non empty TopSpace-like TopStruct
the carrier of S1 is non empty set
bool the carrier of S1 is non empty set
S2 is non empty TopSpace-like TopStruct
the carrier of S2 is non empty set
bool the carrier of S2 is non empty set
T1 is non empty TopSpace-like TopStruct
[:S1,T1:] is non empty strict TopSpace-like TopStruct
the carrier of T1 is non empty set
bool the carrier of T1 is non empty set
T2 is non empty TopSpace-like TopStruct
[:S2,T2:] is non empty strict TopSpace-like TopStruct
the carrier of T2 is non empty set
bool the carrier of T2 is non empty set
the carrier of [:S2,T2:] is non empty set
{ ([:b₁,b₃:] /\ [:b₂,b₄:]) where b₁ is Element of bool the carrier of S1, b₂ is Element of bool the carrier of S2, b₃ is Element of bool the carrier of T1, b₄ is Element of bool the carrier of T2 : ( b₁ is open & b₂ is open & b₃ is open & b₄ is open ) } is set
R1 is non empty TopSpace-like Refinement of [:S1,T1:],[:S2,T2:]
the carrier of R1 is non empty set
bool the carrier of R1 is non empty set
bool (bool the carrier of R1) is non empty set
[: the carrier of S2, the carrier of T2:] is non empty set
the carrier of [:S1,T1:] is non empty set
[: the carrier of S1, the carrier of T1:] is non empty set
the topology of [:S1,T1:] is non empty Element of bool (bool the carrier of [:S1,T1:])
bool the carrier of [:S1,T1:] is non empty set
bool (bool the carrier of [:S1,T1:]) is non empty set
the topology of [:S2,T2:] is non empty Element of bool (bool the carrier of [:S2,T2:])
bool the carrier of [:S2,T2:] is non empty set
bool (bool the carrier of [:S2,T2:]) is non empty set
INTERSECTION ( the topology of [:S1,T1:], the topology of [:S2,T2:]) is set
the carrier of [:S1,T1:] \/ the carrier of [:S2,T2:] is non empty set
[: the carrier of S1, the carrier of T1:] \/ [: the carrier of S2, the carrier of T2:] is non empty set
bool the carrier of R1 is non empty Element of bool (bool the carrier of R1)
C is set
BT is Element of bool the carrier of S1
Bpr is Element of bool the carrier of T1
[:BT,Bpr:] is Element of bool the carrier of [:S1,T1:]
BS is Element of bool the carrier of S2
c is Element of bool the carrier of T2
[:BS,c:] is Element of bool the carrier of [:S2,T2:]
[:BT,Bpr:] /\ [:BS,c:] is Element of bool the carrier of [:S2,T2:]
C is Element of bool (bool the carrier of R1)
the topology of S2 is non empty Element of bool (bool the carrier of S2)
bool (bool the carrier of S2) is non empty set
the topology of T2 is non empty Element of bool (bool the carrier of T2)
bool (bool the carrier of T2) is non empty set
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of S2, b₂ is Element of bool the carrier of T2 : ( b₁ in the topology of S2 & b₂ in the topology of T2 ) } is set
{ (union b₁) where b₁ is Element of bool (bool the carrier of [:S2,T2:]) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of S2, b₃ is Element of bool the carrier of T2 : ( b₁ in the topology of S2 & b₂ in the topology of T2 ) } } is set
the topology of S1 is non empty Element of bool (bool the carrier of S1)
bool (bool the carrier of S1) is non empty set
the topology of T1 is non empty Element of bool (bool the carrier of T1)
bool (bool the carrier of T1) is non empty set
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of S1, b₂ is Element of bool the carrier of T1 : ( b₁ in the topology of S1 & b₂ in the topology of T1 ) } is set
{ (union b₁) where b₁ is Element of bool (bool the carrier of [:S1,T1:]) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of S1, b₃ is Element of bool the carrier of T1 : ( b₁ in the topology of S1 & b₂ in the topology of T1 ) } } is set
BT is Element of bool (bool the carrier of R1)
BS is Element of bool the carrier of R1
Bpr is Element of the carrier of R1
R is non empty open quasi_basis Element of bool (bool the carrier of R1)
c is Element of bool the carrier of R1
a is set
b is set
a /\ b is set
a1 is Element of bool (bool the carrier of [:S1,T1:])
union a1 is Element of bool the carrier of [:S1,T1:]
a2 is set
a2 is Element of bool (bool the carrier of [:S2,T2:])
union a2 is Element of bool the carrier of [:S2,T2:]
a1 is set
b1 is Element of bool the carrier of S2
b2 is Element of bool the carrier of T2
[:b1,b2:] is Element of bool the carrier of [:S2,T2:]
b2 is Element of bool the carrier of S1
b1 is Element of bool the carrier of T1
[:b2,b1:] is Element of bool the carrier of [:S1,T1:]
[:b2,b1:] /\ [:b1,b2:] is Element of bool the carrier of [:S2,T2:]
a is Element of bool the carrier of R1
the topology of R1 is non empty Element of bool (bool the carrier of R1)
BS is set
R is non empty open quasi_basis Element of bool (bool the carrier of R1)
Bpr is Element of bool the carrier of S1
a is Element of bool the carrier of T1
[:Bpr,a:] is Element of bool the carrier of [:S1,T1:]
c is Element of bool the carrier of S2
b is Element of bool the carrier of T2
[:c,b:] is Element of bool the carrier of [:S2,T2:]
[:Bpr,a:] /\ [:c,b:] is Element of bool the carrier of [:S2,T2:]
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
T1 is non empty TopSpace-like TopStruct
[:S1,T1:] is non empty strict TopSpace-like TopStruct
the carrier of T1 is non empty set
T2 is non empty TopSpace-like TopStruct
[:S2,T2:] is non empty strict TopSpace-like TopStruct
the carrier of T2 is non empty set
R1 is non empty TopSpace-like Refinement of [:S1,T1:],[:S2,T2:]
the carrier of R1 is non empty set
the topology of R1 is non empty Element of bool (bool the carrier of R1)
bool the carrier of R1 is non empty set
bool (bool the carrier of R1) is non empty set
R2 is non empty TopSpace-like Refinement of S1,S2
R is non empty TopSpace-like Refinement of T1,T2
[:R2,R:] is non empty strict TopSpace-like TopStruct
the carrier of [:R2,R:] is non empty set
the topology of [:R2,R:] is non empty Element of bool (bool the carrier of [:R2,R:])
bool the carrier of [:R2,R:] is non empty set
bool (bool the carrier of [:R2,R:]) is non empty set
the carrier of R2 is non empty set
the carrier of S1 \/ the carrier of S2 is non empty set
bool the carrier of S1 is non empty set
bool the carrier of S2 is non empty set
bool the carrier of T1 is non empty set
bool the carrier of T2 is non empty set
the carrier of [:S2,T2:] is non empty set
{ ([:b₁,b₃:] /\ [:b₂,b₄:]) where b₁ is Element of bool the carrier of S1, b₂ is Element of bool the carrier of S2, b₃ is Element of bool the carrier of T1, b₄ is Element of bool the carrier of T2 : ( b₁ is open & b₂ is open & b₃ is open & b₄ is open ) } is set
the carrier of R is non empty set
bool the carrier of R is non empty set
bool (bool the carrier of R) is non empty set
the topology of T1 is non empty Element of bool (bool the carrier of T1)
bool (bool the carrier of T1) is non empty set
the topology of T2 is non empty Element of bool (bool the carrier of T2)
bool (bool the carrier of T2) is non empty set
INTERSECTION ( the topology of T1, the topology of T2) is set
bool the carrier of R2 is non empty set
bool (bool the carrier of R2) is non empty set
the topology of S1 is non empty Element of bool (bool the carrier of S1)
bool (bool the carrier of S1) is non empty set
the topology of S2 is non empty Element of bool (bool the carrier of S2)
bool (bool the carrier of S2) is non empty set
INTERSECTION ( the topology of S1, the topology of S2) is set
BS is non empty open quasi_basis Element of bool (bool the carrier of R2)
BT is non empty open quasi_basis Element of bool (bool the carrier of R)
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of R2, b₂ is Element of bool the carrier of R : ( b₁ in BS & b₂ in BT ) } is set
Bpr is non empty open quasi_basis Element of bool (bool the carrier of [:R2,R:])
c is set
a is Element of bool the carrier of S1
a1 is Element of bool the carrier of T1
[:a,a1:] is Element of bool the carrier of [:S1,T1:]
the carrier of [:S1,T1:] is non empty set
bool the carrier of [:S1,T1:] is non empty set
b is Element of bool the carrier of S2
a2 is Element of bool the carrier of T2
[:b,a2:] is Element of bool the carrier of [:S2,T2:]
bool the carrier of [:S2,T2:] is non empty set
[:a,a1:] /\ [:b,a2:] is Element of bool the carrier of [:S2,T2:]
a /\ b is Element of bool the carrier of S2
a1 /\ a2 is Element of bool the carrier of T2
[:(a /\ b),(a1 /\ a2):] is Element of bool the carrier of [:S2,T2:]
c is set
a is Element of bool the carrier of R2
b is Element of bool the carrier of R
[:a,b:] is Element of bool the carrier of [:R2,R:]
a1 is set
a2 is set
a1 /\ a2 is set
a1 is Element of bool the carrier of S1
a2 is Element of bool the carrier of S2
b1 is set
b2 is set
b1 /\ b2 is set
b1 is Element of bool the carrier of T1
b2 is Element of bool the carrier of T2
[:a1,b1:] is Element of bool the carrier of [:S1,T1:]
[:a2,b2:] is Element of bool the carrier of [:S2,T2:]
[:a1,b1:] /\ [:a2,b2:] is Element of bool the carrier of [:S2,T2:]
the carrier of T1 \/ the carrier of T2 is non empty set
the carrier of [:S1,T1:] is non empty set
[: the carrier of S1, the carrier of T1:] is non empty set
the carrier of [:S1,T1:] \/ the carrier of [:S2,T2:] is non empty set
[: the carrier of S2, the carrier of T2:] is non empty set
[: the carrier of S1, the carrier of T1:] \/ [: the carrier of S2, the carrier of T2:] 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
T1 is non empty TopSpace-like TopStruct
the carrier of T1 is non empty set
[:S1,T1:] is non empty strict TopSpace-like TopStruct
T2 is non empty TopSpace-like TopStruct
the carrier of T2 is non empty set
[:S2,T2:] is non empty strict TopSpace-like TopStruct
R1 is non empty TopSpace-like Refinement of S1,S2
R2 is non empty TopSpace-like Refinement of T1,T2
[:R1,R2:] is non empty strict TopSpace-like TopStruct
the non empty strict TopSpace-like Refinement of [:S1,T1:],[:S2,T2:] is non empty strict TopSpace-like Refinement of [:S1,T1:],[:S2,T2:]
the carrier of [:R1,R2:] is non empty set
the carrier of the non empty strict TopSpace-like Refinement of [:S1,T1:],[:S2,T2:] is non empty set