:: 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

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

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

wayabove T1 is Element of bool the carrier of S1

{ b

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

wayabove T2 is Element of bool the carrier of S2

{ b

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

waybelow T1 is Element of bool the carrier of S2

bool the carrier of S2 is non empty set

{ b

T1 is Element of the carrier of S2

waybelow T1 is Element of bool the carrier of S2

{ b

"\/" ((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

"\/" ((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

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

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