K121() is set
bool K121() is non empty set
K141() is set
bool K141() is non empty set
K145() is Element of bool K141()
[:K145(),K145():] is V1() set
[:[:K145(),K145():],K145():] is V1() set
bool [:[:K145(),K145():],K145():] is non empty set
Nat_Lattice is non empty strict LattStr
lcmlat is V1() V4([:K145(),K145():]) V5(K145()) Function-like V18([:K145(),K145():],K145()) Element of bool [:[:K145(),K145():],K145():]
hcflat is V1() V4([:K145(),K145():]) V5(K145()) Function-like V18([:K145(),K145():],K145()) Element of bool [:[:K145(),K145():],K145():]
LattStr(# K145(),lcmlat,hcflat #) is strict LattStr
the carrier of Nat_Lattice is set
bool K145() is non empty set
NATPLUS is Element of bool K145()
[:NATPLUS,NATPLUS:] is V1() set
[:[:NATPLUS,NATPLUS:],NATPLUS:] is V1() set
bool [:[:NATPLUS,NATPLUS:],NATPLUS:] is non empty set
1 is non empty set
{} is set
the V1() V2() V3() empty set is V1() V2() V3() empty set
T is 1-sorted
the carrier of T is set
bool the carrier of T is non empty set
[#] T is Element of bool the carrier of T
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
L \/ OL is Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
([#] T) \ L is Element of bool the carrier of T
OL \ L is Element of bool the carrier of T
L \/ (L `) is Element of bool the carrier of T
T is 1-sorted
the carrier of T is set
bool the carrier of T is non empty set
A is 1-sorted
the carrier of A is set
bool the carrier of A is non empty set
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
C is Element of bool the carrier of A
B is Element of bool the carrier of A
B ` is Element of bool the carrier of A
the carrier of A \ B is set
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
Cl (Int (Cl L)) is closed Element of bool the carrier of T
Cl (Cl L) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Int L is open Element of bool the carrier of T
Cl (Int L) is closed Element of bool the carrier of T
Int (Cl (Int L)) is open Element of bool the carrier of T
Int (Int L) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
Cl (Int (Cl L)) is closed Element of bool the carrier of T
Int (Cl (Int (Cl L))) is open Element of bool the carrier of T
Int (Int (Cl L)) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
Int L is open Element of bool the carrier of T
Cl (Int L) is closed Element of bool the carrier of T
Int OL is open Element of bool the carrier of T
Cl (Int OL) is closed Element of bool the carrier of T
(Cl (Int L)) \/ (Cl (Int OL)) is closed Element of bool the carrier of T
L \/ OL is Element of bool the carrier of T
Int (L \/ OL) is open Element of bool the carrier of T
Cl (Int (L \/ OL)) is closed Element of bool the carrier of T
(L \/ OL) ` is Element of bool the carrier of T
the carrier of T \ (L \/ OL) is set
(L \/ OL) \/ ((L \/ OL) `) is Element of bool the carrier of T
Cl ((L \/ OL) `) is closed Element of bool the carrier of T
(L \/ OL) \/ (Cl ((L \/ OL) `)) is Element of bool the carrier of T
[#] T is open closed dense Element of bool the carrier of T
OL \/ (Cl ((L \/ OL) `)) is Element of bool the carrier of T
L \/ (OL \/ (Cl ((L \/ OL) `))) is Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
Cl (L `) is closed Element of bool the carrier of T
Cl (OL \/ (Cl ((L \/ OL) `))) is closed Element of bool the carrier of T
L \/ (Cl ((L \/ OL) `)) is Element of bool the carrier of T
OL \/ (L \/ (Cl ((L \/ OL) `))) is Element of bool the carrier of T
OL ` is Element of bool the carrier of T
the carrier of T \ OL is set
Cl (OL `) is closed Element of bool the carrier of T
Cl (L \/ (Cl ((L \/ OL) `))) is closed Element of bool the carrier of T
(Cl (OL `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (OL `)) is set
((Cl (OL `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl (OL `)) `) is set
OL \/ L is Element of bool the carrier of T
(OL \/ L) ` is Element of bool the carrier of T
the carrier of T \ (OL \/ L) is set
Cl ((OL \/ L) `) is closed Element of bool the carrier of T
L \/ (Cl ((OL \/ L) `)) is Element of bool the carrier of T
((Cl (OL `)) `) \/ (L \/ (Cl ((OL \/ L) `))) is Element of bool the carrier of T
(Int OL) \/ (L \/ (Cl ((OL \/ L) `))) is Element of bool the carrier of T
(Int OL) \/ (Cl ((OL \/ L) `)) is Element of bool the carrier of T
L \/ ((Int OL) \/ (Cl ((OL \/ L) `))) is Element of bool the carrier of T
Cl ((Int OL) \/ (Cl ((OL \/ L) `))) is closed Element of bool the carrier of T
Cl (Cl ((OL \/ L) `)) is closed Element of bool the carrier of T
(Cl (Int OL)) \/ (Cl (Cl ((OL \/ L) `))) is closed Element of bool the carrier of T
(Cl (L `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (L `)) is set
(Cl (L `)) \/ ((Cl (L `)) `) is Element of bool the carrier of T
(Cl (Int OL)) \/ (Cl ((OL \/ L) `)) is closed Element of bool the carrier of T
((Cl (Int OL)) \/ (Cl ((OL \/ L) `))) \/ ((Cl (L `)) `) is Element of bool the carrier of T
(Cl ((OL \/ L) `)) \/ (Cl (Int OL)) is closed Element of bool the carrier of T
((Cl ((OL \/ L) `)) \/ (Cl (Int OL))) \/ (Int L) is Element of bool the carrier of T
(Cl (Int OL)) \/ (Int L) is Element of bool the carrier of T
(Cl ((OL \/ L) `)) \/ ((Cl (Int OL)) \/ (Int L)) is Element of bool the carrier of T
(Cl ((OL \/ L) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((OL \/ L) `)) is set
Int (OL \/ L) is open Element of bool the carrier of T
Cl (Int (OL \/ L)) is closed Element of bool the carrier of T
Cl ((Cl (Int OL)) \/ (Int L)) is closed Element of bool the carrier of T
Cl (Cl (Int OL)) is closed Element of bool the carrier of T
(Cl (Cl (Int OL))) \/ (Cl (Int L)) is closed Element of bool the carrier of T
(Cl (L `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (L `)) is set
((Cl (L `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl (L `)) `) is set
((Cl (L `)) `) \/ (OL \/ (Cl ((L \/ OL) `))) is Element of bool the carrier of T
(Int L) \/ (OL \/ (Cl ((L \/ OL) `))) is Element of bool the carrier of T
(Int L) \/ (Cl ((L \/ OL) `)) is Element of bool the carrier of T
OL \/ ((Int L) \/ (Cl ((L \/ OL) `))) is Element of bool the carrier of T
Cl ((Int L) \/ (Cl ((L \/ OL) `))) is closed Element of bool the carrier of T
Cl (Cl ((L \/ OL) `)) is closed Element of bool the carrier of T
(Cl (Int L)) \/ (Cl (Cl ((L \/ OL) `))) is closed Element of bool the carrier of T
(Cl (OL `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (OL `)) is set
(Cl (OL `)) \/ ((Cl (OL `)) `) is Element of bool the carrier of T
(Cl (Int L)) \/ (Cl ((L \/ OL) `)) is closed Element of bool the carrier of T
((Cl (Int L)) \/ (Cl ((L \/ OL) `))) \/ ((Cl (OL `)) `) is Element of bool the carrier of T
(Cl ((L \/ OL) `)) \/ (Cl (Int L)) is closed Element of bool the carrier of T
((Cl ((L \/ OL) `)) \/ (Cl (Int L))) \/ (Int OL) is Element of bool the carrier of T
(Cl (Int L)) \/ (Int OL) is Element of bool the carrier of T
(Cl ((L \/ OL) `)) \/ ((Cl (Int L)) \/ (Int OL)) is Element of bool the carrier of T
(Cl ((L \/ OL) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((L \/ OL) `)) is set
Cl ((Cl (Int L)) \/ (Int OL)) is closed Element of bool the carrier of T
Cl (Cl (Int L)) is closed Element of bool the carrier of T
(Cl (Cl (Int L))) \/ (Cl (Int OL)) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
Cl OL is closed Element of bool the carrier of T
Int (Cl OL) is open Element of bool the carrier of T
(Int (Cl L)) /\ (Int (Cl OL)) is open Element of bool the carrier of T
L /\ OL is Element of bool the carrier of T
Cl (L /\ OL) is closed Element of bool the carrier of T
Int (Cl (L /\ OL)) is open Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
Int (L `) is open Element of bool the carrier of T
(Int (L `)) ` is closed Element of bool the carrier of T
the carrier of T \ (Int (L `)) is set
OL ` is Element of bool the carrier of T
the carrier of T \ OL is set
Int (OL `) is open Element of bool the carrier of T
(Int (OL `)) ` is closed Element of bool the carrier of T
the carrier of T \ (Int (OL `)) is set
(L /\ OL) ` is Element of bool the carrier of T
the carrier of T \ (L /\ OL) is set
{} T is Element of bool the carrier of T
(L /\ OL) /\ ((L /\ OL) `) is Element of bool the carrier of T
Int ((L /\ OL) `) is open Element of bool the carrier of T
(L /\ OL) /\ (Int ((L /\ OL) `)) is Element of bool the carrier of T
OL /\ (Int ((L /\ OL) `)) is Element of bool the carrier of T
L /\ (OL /\ (Int ((L /\ OL) `))) is Element of bool the carrier of T
Int (OL /\ (Int ((L /\ OL) `))) is open Element of bool the carrier of T
L /\ (Int ((L /\ OL) `)) is Element of bool the carrier of T
OL /\ (L /\ (Int ((L /\ OL) `))) is Element of bool the carrier of T
Int (L /\ (Int ((L /\ OL) `))) is open Element of bool the carrier of T
((Int (OL `)) `) ` is open Element of bool the carrier of T
the carrier of T \ ((Int (OL `)) `) is set
((Int (OL `)) `) /\ (L /\ (Int ((L /\ OL) `))) is Element of bool the carrier of T
(OL `) ` is Element of bool the carrier of T
the carrier of T \ (OL `) is set
Cl ((OL `) `) is closed Element of bool the carrier of T
(Cl ((OL `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((OL `) `)) is set
((Cl ((OL `) `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl ((OL `) `)) `) is set
(((Cl ((OL `) `)) `) `) /\ (L /\ (Int ((L /\ OL) `))) is Element of bool the carrier of T
(Cl OL) /\ (Int ((L /\ OL) `)) is Element of bool the carrier of T
L /\ ((Cl OL) /\ (Int ((L /\ OL) `))) is Element of bool the carrier of T
Int ((Cl OL) /\ (Int ((L /\ OL) `))) is open Element of bool the carrier of T
Int (Int ((L /\ OL) `)) is open Element of bool the carrier of T
(Int (Cl OL)) /\ (Int (Int ((L /\ OL) `))) is open Element of bool the carrier of T
(Int (Cl OL)) /\ (Int ((L /\ OL) `)) is open Element of bool the carrier of T
((Int (Cl OL)) /\ (Int ((L /\ OL) `))) /\ ((Int (L `)) `) is Element of bool the carrier of T
(Int (L `)) /\ ((Int (L `)) `) is Element of bool the carrier of T
(L `) ` is Element of bool the carrier of T
the carrier of T \ (L `) is set
Cl ((L `) `) is closed Element of bool the carrier of T
(Cl ((L `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((L `) `)) is set
((Cl ((L `) `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl ((L `) `)) `) is set
((Int (Cl OL)) /\ (Int ((L /\ OL) `))) /\ (((Cl ((L `) `)) `) `) is Element of bool the carrier of T
(Int (Cl OL)) /\ (Cl L) is Element of bool the carrier of T
(Int ((L /\ OL) `)) /\ ((Int (Cl OL)) /\ (Cl L)) is Element of bool the carrier of T
(Int ((L /\ OL) `)) ` is closed Element of bool the carrier of T
the carrier of T \ (Int ((L /\ OL) `)) is set
((L /\ OL) `) ` is Element of bool the carrier of T
the carrier of T \ ((L /\ OL) `) is set
Cl (((L /\ OL) `) `) is closed Element of bool the carrier of T
(Cl (((L /\ OL) `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (((L /\ OL) `) `)) is set
((Cl (((L /\ OL) `) `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl (((L /\ OL) `) `)) `) is set
Int ((Int (Cl OL)) /\ (Cl L)) is open Element of bool the carrier of T
OL /\ L is Element of bool the carrier of T
Cl (OL /\ L) is closed Element of bool the carrier of T
Int (Cl (OL /\ L)) is open Element of bool the carrier of T
Int (Int (Cl OL)) is open Element of bool the carrier of T
(Int (Int (Cl OL))) /\ (Int (Cl L)) is open Element of bool the carrier of T
((Int (L `)) `) ` is open Element of bool the carrier of T
the carrier of T \ ((Int (L `)) `) is set
((Int (L `)) `) /\ (OL /\ (Int ((L /\ OL) `))) is Element of bool the carrier of T
(L `) ` is Element of bool the carrier of T
the carrier of T \ (L `) is set
Cl ((L `) `) is closed Element of bool the carrier of T
(Cl ((L `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((L `) `)) is set
((Cl ((L `) `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl ((L `) `)) `) is set
(((Cl ((L `) `)) `) `) /\ (OL /\ (Int ((L /\ OL) `))) is Element of bool the carrier of T
(Cl L) /\ (Int ((L /\ OL) `)) is Element of bool the carrier of T
OL /\ ((Cl L) /\ (Int ((L /\ OL) `))) is Element of bool the carrier of T
Int ((Cl L) /\ (Int ((L /\ OL) `))) is open Element of bool the carrier of T
Int (Int ((L /\ OL) `)) is open Element of bool the carrier of T
(Int (Cl L)) /\ (Int (Int ((L /\ OL) `))) is open Element of bool the carrier of T
(Int (Cl L)) /\ (Int ((L /\ OL) `)) is open Element of bool the carrier of T
((Int (Cl L)) /\ (Int ((L /\ OL) `))) /\ ((Int (OL `)) `) is Element of bool the carrier of T
(Int (OL `)) /\ ((Int (OL `)) `) is Element of bool the carrier of T
(OL `) ` is Element of bool the carrier of T
the carrier of T \ (OL `) is set
Cl ((OL `) `) is closed Element of bool the carrier of T
(Cl ((OL `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((OL `) `)) is set
((Cl ((OL `) `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl ((OL `) `)) `) is set
((Int (Cl L)) /\ (Int ((L /\ OL) `))) /\ (((Cl ((OL `) `)) `) `) is Element of bool the carrier of T
(Int (Cl L)) /\ (Cl OL) is Element of bool the carrier of T
(Int ((L /\ OL) `)) /\ ((Int (Cl L)) /\ (Cl OL)) is Element of bool the carrier of T
(Int ((L /\ OL) `)) ` is closed Element of bool the carrier of T
the carrier of T \ (Int ((L /\ OL) `)) is set
((L /\ OL) `) ` is Element of bool the carrier of T
the carrier of T \ ((L /\ OL) `) is set
Cl (((L /\ OL) `) `) is closed Element of bool the carrier of T
(Cl (((L /\ OL) `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (((L /\ OL) `) `)) is set
((Cl (((L /\ OL) `) `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl (((L /\ OL) `) `)) `) is set
Int ((Int (Cl L)) /\ (Cl OL)) is open Element of bool the carrier of T
Int (Int (Cl L)) is open Element of bool the carrier of T
(Int (Int (Cl L))) /\ (Int (Cl OL)) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
{} T is Element of bool the carrier of T
L is Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
Cl (L `) is closed Element of bool the carrier of T
L /\ (Cl (L `)) is Element of bool the carrier of T
Int (L /\ (Cl (L `))) is open Element of bool the carrier of T
Int L is open Element of bool the carrier of T
(Int L) ` is closed Element of bool the carrier of T
the carrier of T \ (Int L) is set
(Cl (L `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (L `)) is set
((Cl (L `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl (L `)) `) is set
L /\ (((Cl (L `)) `) `) is Element of bool the carrier of T
Int (L /\ (((Cl (L `)) `) `)) is open Element of bool the carrier of T
L /\ ((Int L) `) is Element of bool the carrier of T
Int (L /\ ((Int L) `)) is open Element of bool the carrier of T
Int (Int L) is open Element of bool the carrier of T
Int ((Int L) `) is open Element of bool the carrier of T
(Int (Int L)) /\ (Int ((Int L) `)) is open Element of bool the carrier of T
(Int L) /\ ((Int L) `) is Element of bool the carrier of T
Int ((Int L) /\ ((Int L) `)) is open Element of bool the carrier of T
Int ({} T) is V1() V2() V3() empty open closed boundary nowhere_dense Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
[#] T is open closed dense Element of bool the carrier of T
L is Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
Int (L `) is open Element of bool the carrier of T
L \/ (Int (L `)) is Element of bool the carrier of T
Cl (L \/ (Int (L `))) is closed Element of bool the carrier of T
(L `) ` is Element of bool the carrier of T
the carrier of T \ (L `) is set
Cl ((L `) `) is closed Element of bool the carrier of T
(Cl ((L `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((L `) `)) is set
L \/ ((Cl ((L `) `)) `) is Element of bool the carrier of T
Cl (L \/ ((Cl ((L `) `)) `)) is closed Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Cl (Cl L) is closed Element of bool the carrier of T
(Cl L) ` is open Element of bool the carrier of T
the carrier of T \ (Cl L) is set
Cl ((Cl L) `) is closed Element of bool the carrier of T
(Cl (Cl L)) \/ (Cl ((Cl L) `)) is closed Element of bool the carrier of T
(Cl L) \/ ((Cl L) `) is Element of bool the carrier of T
Cl ((Cl L) \/ ((Cl L) `)) is closed Element of bool the carrier of T
Cl ([#] T) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
Cl OL is closed Element of bool the carrier of T
Int (Cl OL) is open Element of bool the carrier of T
(Int (Cl OL)) \/ OL is Element of bool the carrier of T
L \/ ((Int (Cl OL)) \/ OL) is Element of bool the carrier of T
Cl (L \/ ((Int (Cl OL)) \/ OL)) is closed Element of bool the carrier of T
Int (Cl (L \/ ((Int (Cl OL)) \/ OL))) is open Element of bool the carrier of T
(Int (Cl (L \/ ((Int (Cl OL)) \/ OL)))) \/ (L \/ ((Int (Cl OL)) \/ OL)) is Element of bool the carrier of T
L \/ OL is Element of bool the carrier of T
Cl (L \/ OL) is closed Element of bool the carrier of T
Int (Cl (L \/ OL)) is open Element of bool the carrier of T
(Int (Cl (L \/ OL))) \/ (L \/ OL) is Element of bool the carrier of T
(Int (Cl (L \/ ((Int (Cl OL)) \/ OL)))) \/ (Int (Cl OL)) is open Element of bool the carrier of T
L \/ (Int (Cl OL)) is Element of bool the carrier of T
(L \/ (Int (Cl OL))) \/ OL is Element of bool the carrier of T
Cl ((L \/ (Int (Cl OL))) \/ OL) is closed Element of bool the carrier of T
Int (Cl ((L \/ (Int (Cl OL))) \/ OL)) is open Element of bool the carrier of T
Cl (L \/ (Int (Cl OL))) is closed Element of bool the carrier of T
(Cl (L \/ (Int (Cl OL)))) \/ (Cl OL) is closed Element of bool the carrier of T
Int ((Cl (L \/ (Int (Cl OL)))) \/ (Cl OL)) is open Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Cl (Int (Cl OL)) is closed Element of bool the carrier of T
(Cl L) \/ (Cl (Int (Cl OL))) is closed Element of bool the carrier of T
((Cl L) \/ (Cl (Int (Cl OL)))) \/ (Cl OL) is closed Element of bool the carrier of T
Int (((Cl L) \/ (Cl (Int (Cl OL)))) \/ (Cl OL)) is open Element of bool the carrier of T
(Cl (Int (Cl OL))) \/ (Cl OL) is closed Element of bool the carrier of T
(Cl L) \/ ((Cl (Int (Cl OL))) \/ (Cl OL)) is closed Element of bool the carrier of T
Int ((Cl L) \/ ((Cl (Int (Cl OL))) \/ (Cl OL))) is open Element of bool the carrier of T
(Cl L) \/ (Cl OL) is closed Element of bool the carrier of T
Int ((Cl L) \/ (Cl OL)) is open Element of bool the carrier of T
(Int (Cl OL)) \/ (L \/ OL) is Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
(Int (Cl L)) \/ L is Element of bool the carrier of T
OL is Element of bool the carrier of T
((Int (Cl L)) \/ L) \/ OL is Element of bool the carrier of T
Cl (((Int (Cl L)) \/ L) \/ OL) is closed Element of bool the carrier of T
Int (Cl (((Int (Cl L)) \/ L) \/ OL)) is open Element of bool the carrier of T
(Int (Cl (((Int (Cl L)) \/ L) \/ OL))) \/ (((Int (Cl L)) \/ L) \/ OL) is Element of bool the carrier of T
L \/ OL is Element of bool the carrier of T
Cl (L \/ OL) is closed Element of bool the carrier of T
Int (Cl (L \/ OL)) is open Element of bool the carrier of T
(Int (Cl (L \/ OL))) \/ (L \/ OL) is Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
Int OL is open Element of bool the carrier of T
Cl (Int OL) is closed Element of bool the carrier of T
(Cl (Int OL)) /\ OL is Element of bool the carrier of T
L /\ ((Cl (Int OL)) /\ OL) is Element of bool the carrier of T
Int (L /\ ((Cl (Int OL)) /\ OL)) is open Element of bool the carrier of T
Cl (Int (L /\ ((Cl (Int OL)) /\ OL))) is closed Element of bool the carrier of T
(Cl (Int (L /\ ((Cl (Int OL)) /\ OL)))) /\ (L /\ ((Cl (Int OL)) /\ OL)) is Element of bool the carrier of T
L /\ OL is Element of bool the carrier of T
Int (L /\ OL) is open Element of bool the carrier of T
Cl (Int (L /\ OL)) is closed Element of bool the carrier of T
(Cl (Int (L /\ OL))) /\ (L /\ OL) is Element of bool the carrier of T
L /\ (Cl (Int OL)) is Element of bool the carrier of T
(L /\ (Cl (Int OL))) /\ OL is Element of bool the carrier of T
Int ((L /\ (Cl (Int OL))) /\ OL) is open Element of bool the carrier of T
Cl (Int ((L /\ (Cl (Int OL))) /\ OL)) is closed Element of bool the carrier of T
Int (L /\ (Cl (Int OL))) is open Element of bool the carrier of T
(Int (L /\ (Cl (Int OL)))) /\ (Int OL) is open Element of bool the carrier of T
Cl ((Int (L /\ (Cl (Int OL)))) /\ (Int OL)) is closed Element of bool the carrier of T
Int L is open Element of bool the carrier of T
Int (Cl (Int OL)) is open Element of bool the carrier of T
(Int L) /\ (Int (Cl (Int OL))) is open Element of bool the carrier of T
((Int L) /\ (Int (Cl (Int OL)))) /\ (Int OL) is open Element of bool the carrier of T
Cl (((Int L) /\ (Int (Cl (Int OL)))) /\ (Int OL)) is closed Element of bool the carrier of T
(Int (Cl (Int OL))) /\ (Int OL) is open Element of bool the carrier of T
(Int L) /\ ((Int (Cl (Int OL))) /\ (Int OL)) is open Element of bool the carrier of T
Cl ((Int L) /\ ((Int (Cl (Int OL))) /\ (Int OL))) is closed Element of bool the carrier of T
(Int L) /\ (Int OL) is open Element of bool the carrier of T
Cl ((Int L) /\ (Int OL)) is closed Element of bool the carrier of T
(Cl (Int (L /\ ((Cl (Int OL)) /\ OL)))) /\ (Cl (Int OL)) is closed Element of bool the carrier of T
(Cl (Int OL)) /\ (L /\ OL) is Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Int L is open Element of bool the carrier of T
Cl (Int L) is closed Element of bool the carrier of T
(Cl (Int L)) /\ L is Element of bool the carrier of T
OL is Element of bool the carrier of T
((Cl (Int L)) /\ L) /\ OL is Element of bool the carrier of T
Int (((Cl (Int L)) /\ L) /\ OL) is open Element of bool the carrier of T
Cl (Int (((Cl (Int L)) /\ L) /\ OL)) is closed Element of bool the carrier of T
(Cl (Int (((Cl (Int L)) /\ L) /\ OL))) /\ (((Cl (Int L)) /\ L) /\ OL) is Element of bool the carrier of T
L /\ OL is Element of bool the carrier of T
Int (L /\ OL) is open Element of bool the carrier of T
Cl (Int (L /\ OL)) is closed Element of bool the carrier of T
(Cl (Int (L /\ OL))) /\ (L /\ OL) is Element of bool the carrier of T
T is TopSpace-like TopStruct
{} T is Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
Int ({} T) is V1() V2() V3() empty open closed boundary nowhere_dense Element of bool the carrier of T
Cl ({} T) is closed Element of bool the carrier of T
Int (Cl ({} T)) is open Element of bool the carrier of T
Cl (Int ({} T)) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
[#] T is open closed dense Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
Cl ([#] T) is closed Element of bool the carrier of T
Int ([#] T) is open Element of bool the carrier of T
Cl (Int ([#] T)) is closed Element of bool the carrier of T
Int (Cl ([#] T)) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
Int L is open Element of bool the carrier of T
Cl (Int L) is closed Element of bool the carrier of T
(Int L) ` is closed Element of bool the carrier of T
the carrier of T \ (Int L) is set
((Int L) `) ` is open Element of bool the carrier of T
the carrier of T \ ((Int L) `) is set
Cl (((Int L) `) `) is closed Element of bool the carrier of T
(Cl (((Int L) `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (((Int L) `) `)) is set
Int ((Int L) `) is open Element of bool the carrier of T
Cl (L `) is closed Element of bool the carrier of T
(Cl (L `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (L `)) is set
((Cl (L `)) `) ` is closed Element of bool the carrier of T
the carrier of T \ ((Cl (L `)) `) is set
Int (((Cl (L `)) `) `) is open Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
(Cl L) ` is open Element of bool the carrier of T
the carrier of T \ (Cl L) is set
Cl ((Cl L) `) is closed Element of bool the carrier of T
(Cl ((Cl L) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl L) `)) is set
(L `) ` is Element of bool the carrier of T
the carrier of T \ (L `) is set
Cl ((L `) `) is closed Element of bool the carrier of T
(Cl ((L `) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((L `) `)) is set
Cl ((Cl ((L `) `)) `) is closed Element of bool the carrier of T
Int (L `) is open Element of bool the carrier of T
Cl (Int (L `)) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
L \/ OL is Element of bool the carrier of T
Cl (L \/ OL) is closed Element of bool the carrier of T
Int (Cl (L \/ OL)) is open Element of bool the carrier of T
(Int (Cl (L \/ OL))) \/ (L \/ OL) is Element of bool the carrier of T
L /\ OL is Element of bool the carrier of T
Int (L /\ OL) is open Element of bool the carrier of T
Cl (Int (L /\ OL)) is closed Element of bool the carrier of T
(Cl (Int (L /\ OL))) /\ (L /\ OL) is Element of bool the carrier of T
Int OL is open Element of bool the carrier of T
Cl (Int OL) is closed Element of bool the carrier of T
Int L is open Element of bool the carrier of T
Cl (Int L) is closed Element of bool the carrier of T
(Int L) \/ (Int OL) is open Element of bool the carrier of T
Cl ((Int L) \/ (Int OL)) is closed Element of bool the carrier of T
Int (L \/ OL) is open Element of bool the carrier of T
Cl (Int (L \/ OL)) is closed Element of bool the carrier of T
(Cl (Int L)) \/ (Cl (Int OL)) is closed Element of bool the carrier of T
(Int (Cl (L \/ OL))) \/ (Cl (Int (L \/ OL))) is Element of bool the carrier of T
Int (Int (Cl (L \/ OL))) is open Element of bool the carrier of T
(Int (Int (Cl (L \/ OL)))) \/ (Int (L \/ OL)) is open Element of bool the carrier of T
Cl ((Int (Int (Cl (L \/ OL)))) \/ (Int (L \/ OL))) is closed Element of bool the carrier of T
Int ((Int (Cl (L \/ OL))) \/ (L \/ OL)) is open Element of bool the carrier of T
Cl (Int ((Int (Cl (L \/ OL))) \/ (L \/ OL))) is closed Element of bool the carrier of T
Cl (Int (Cl (L \/ OL))) is closed Element of bool the carrier of T
(Cl (Int (Cl (L \/ OL)))) \/ (Cl (Int (L \/ OL))) is closed Element of bool the carrier of T
Cl (Cl (L \/ OL)) is closed Element of bool the carrier of T
(Cl (Int (Cl (L \/ OL)))) \/ (Cl (L \/ OL)) is closed Element of bool the carrier of T
Cl ((Int (Cl (L \/ OL))) \/ (L \/ OL)) is closed Element of bool the carrier of T
Int (Cl ((Int (Cl (L \/ OL))) \/ (L \/ OL))) is open Element of bool the carrier of T
Cl OL is closed Element of bool the carrier of T
Int (Cl OL) is open Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
Cl (L /\ OL) is closed Element of bool the carrier of T
Int (Cl (L /\ OL)) is open Element of bool the carrier of T
(Cl L) /\ (Cl OL) is closed Element of bool the carrier of T
Int ((Cl L) /\ (Cl OL)) is open Element of bool the carrier of T
(Int (Cl L)) /\ (Int (Cl OL)) is open Element of bool the carrier of T
(Cl (Int (L /\ OL))) /\ (Int (Cl (L /\ OL))) is Element of bool the carrier of T
Cl ((Cl (Int (L /\ OL))) /\ (L /\ OL)) is closed Element of bool the carrier of T
Int (Cl ((Cl (Int (L /\ OL))) /\ (L /\ OL))) is open Element of bool the carrier of T
Cl (Cl (Int (L /\ OL))) is closed Element of bool the carrier of T
(Cl (Cl (Int (L /\ OL)))) /\ (Cl (L /\ OL)) is closed Element of bool the carrier of T
Int ((Cl (Cl (Int (L /\ OL)))) /\ (Cl (L /\ OL))) is open Element of bool the carrier of T
Int (Cl (Int (L /\ OL))) is open Element of bool the carrier of T
(Int (Cl (Int (L /\ OL)))) /\ (Int (Cl (L /\ OL))) is open Element of bool the carrier of T
Int (Int (L /\ OL)) is open Element of bool the carrier of T
(Int (Cl (Int (L /\ OL)))) /\ (Int (L /\ OL)) is open Element of bool the carrier of T
Int ((Cl (Int (L /\ OL))) /\ (L /\ OL)) is open Element of bool the carrier of T
Cl (Int ((Cl (Int (L /\ OL))) /\ (L /\ OL))) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
{} T is Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
Int ({} T) is V1() V2() V3() empty open closed boundary nowhere_dense Element of bool the carrier of T
Cl (Int ({} T)) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
[#] T is open closed dense Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
Int ([#] T) is open Element of bool the carrier of T
Cl (Int ([#] T)) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
{} T is Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
Cl ({} T) is closed Element of bool the carrier of T
Int (Cl ({} T)) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
[#] T is open closed dense Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
Cl ([#] T) is closed Element of bool the carrier of T
Int (Cl ([#] T)) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Int L is open Element of bool the carrier of T
Cl (Int L) is closed Element of bool the carrier of T
Int (Cl (Int L)) is open Element of bool the carrier of T
Cl (Int (Cl (Int L))) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
Cl (Int (Cl L)) is closed Element of bool the carrier of T
Int (Cl (Int (Cl L))) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
Cl (Int (Cl L)) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
Int L is open Element of bool the carrier of T
Cl (Int L) is closed Element of bool the carrier of T
Int (Cl (Int L)) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
Cl (L `) is closed Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
L ` is Element of bool the carrier of T
the carrier of T \ L is set
Int (L `) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
A is Element of bool the carrier of T
OL /\ A is Element of bool the carrier of T
Int (OL /\ A) is open Element of bool the carrier of T
Cl (Int (OL /\ A)) is closed Element of bool the carrier of T
L /\ (Cl (Int (OL /\ A))) is Element of bool the carrier of T
Int (L /\ (Cl (Int (OL /\ A)))) is open Element of bool the carrier of T
Cl (Int (L /\ (Cl (Int (OL /\ A))))) is closed Element of bool the carrier of T
L /\ OL is Element of bool the carrier of T
Int (L /\ OL) is open Element of bool the carrier of T
Cl (Int (L /\ OL)) is closed Element of bool the carrier of T
(Cl (Int (L /\ OL))) /\ A is Element of bool the carrier of T
Int ((Cl (Int (L /\ OL))) /\ A) is open Element of bool the carrier of T
Cl (Int ((Cl (Int (L /\ OL))) /\ A)) is closed Element of bool the carrier of T
Int OL is open Element of bool the carrier of T
Cl (Int OL) is closed Element of bool the carrier of T
(L /\ OL) /\ A is Element of bool the carrier of T
Int A is open Element of bool the carrier of T
(Int OL) /\ (Int A) is open Element of bool the carrier of T
Cl ((Int OL) /\ (Int A)) is closed Element of bool the carrier of T
Cl (Int A) is closed Element of bool the carrier of T
L /\ (OL /\ A) is Element of bool the carrier of T
Int (Int (L /\ (Cl (Int (OL /\ A))))) is open Element of bool the carrier of T
Int L is open Element of bool the carrier of T
(Int L) /\ (Int OL) is open Element of bool the carrier of T
Cl ((Int L) /\ (Int OL)) is closed Element of bool the carrier of T
Cl (Int L) is closed Element of bool the carrier of T
Int (Int ((Cl (Int (L /\ OL))) /\ A)) is open Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
L is Element of bool the carrier of T
OL is Element of bool the carrier of T
A is Element of bool the carrier of T
OL \/ A is Element of bool the carrier of T
Cl (OL \/ A) is closed Element of bool the carrier of T
Int (Cl (OL \/ A)) is open Element of bool the carrier of T
L \/ (Int (Cl (OL \/ A))) is Element of bool the carrier of T
Cl (L \/ (Int (Cl (OL \/ A)))) is closed Element of bool the carrier of T
Int (Cl (L \/ (Int (Cl (OL \/ A))))) is open Element of bool the carrier of T
L \/ OL is Element of bool the carrier of T
Cl (L \/ OL) is closed Element of bool the carrier of T
Int (Cl (L \/ OL)) is open Element of bool the carrier of T
(Int (Cl (L \/ OL))) \/ A is Element of bool the carrier of T
Cl ((Int (Cl (L \/ OL))) \/ A) is closed Element of bool the carrier of T
Int (Cl ((Int (Cl (L \/ OL))) \/ A)) is open Element of bool the carrier of T
Cl OL is closed Element of bool the carrier of T
Int (Cl OL) is open Element of bool the carrier of T
(L \/ OL) \/ A is Element of bool the carrier of T
Cl A is closed Element of bool the carrier of T
(Cl OL) \/ (Cl A) is closed Element of bool the carrier of T
Int ((Cl OL) \/ (Cl A)) is open Element of bool the carrier of T
Int (Cl A) is open Element of bool the carrier of T
L \/ (OL \/ A) is Element of bool the carrier of T
Cl (Cl (L \/ (Int (Cl (OL \/ A))))) is closed Element of bool the carrier of T
Cl L is closed Element of bool the carrier of T
(Cl L) \/ (Cl OL) is closed Element of bool the carrier of T
Int ((Cl L) \/ (Cl OL)) is open Element of bool the carrier of T
Int (Cl L) is open Element of bool the carrier of T
Cl (Cl ((Int (Cl (L \/ OL))) \/ A)) is closed Element of bool the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
bool (bool the carrier of T) is non empty set
OL is set
A is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
{} T is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
OL is Element of [:(T),(T):]
OL `1 is Element of (T)
OL `2 is Element of (T)
B is Element of (T)
A is Element of (T)
A \/ B is Element of bool the carrier of T
Cl (A \/ B) is closed Element of bool the carrier of T
Int (Cl (A \/ B)) is open Element of bool the carrier of T
(Int (Cl (A \/ B))) \/ (A \/ B) is Element of bool the carrier of T
C is Element of bool the carrier of T
A is Element of bool the carrier of T
C is Element of (T)
A is Element of (T)
a is Element of (T)
[A,a] is Element of [:(T),(T):]
{A,a} is set
{A} is set
{{A,a},{A}} is set
A \/ a is Element of bool the carrier of T
Cl (A \/ a) is closed Element of bool the carrier of T
Int (Cl (A \/ a)) is open Element of bool the carrier of T
(Int (Cl (A \/ a))) \/ (A \/ a) is Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
OL . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL . [A,B] is set
A \/ B is Element of bool the carrier of T
Cl (A \/ B) is closed Element of bool the carrier of T
Int (Cl (A \/ B)) is open Element of bool the carrier of T
(Int (Cl (A \/ B))) \/ (A \/ B) is Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
OL . [A,B] is Element of (T)
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
OL is Element of [:(T),(T):]
OL `1 is Element of (T)
OL `2 is Element of (T)
B is Element of (T)
A is Element of (T)
A /\ B is Element of bool the carrier of T
Int (A /\ B) is open Element of bool the carrier of T
Cl (Int (A /\ B)) is closed Element of bool the carrier of T
(Cl (Int (A /\ B))) /\ (A /\ B) is Element of bool the carrier of T
C is Element of bool the carrier of T
A is Element of bool the carrier of T
C is Element of (T)
A is Element of (T)
a is Element of (T)
[A,a] is Element of [:(T),(T):]
{A,a} is set
{A} is set
{{A,a},{A}} is set
A /\ a is Element of bool the carrier of T
Int (A /\ a) is open Element of bool the carrier of T
Cl (Int (A /\ a)) is closed Element of bool the carrier of T
(Cl (Int (A /\ a))) /\ (A /\ a) is Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
OL . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL . [A,B] is set
A /\ B is Element of bool the carrier of T
Int (A /\ B) is open Element of bool the carrier of T
Cl (Int (A /\ B)) is closed Element of bool the carrier of T
(Cl (Int (A /\ B))) /\ (A /\ B) is Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
OL . [A,B] is Element of (T)
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
A "\/" OL is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (A,OL) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,OL] is set
{A,OL} is set
{A} is set
{{A,OL},{A}} is set
the L_join of LattStr(# (T),(T),(T) #) . [A,OL] is set
C is Element of (T)
B is Element of (T)
C \/ B is Element of bool the carrier of T
Cl (C \/ B) is closed Element of bool the carrier of T
Int (Cl (C \/ B)) is open Element of bool the carrier of T
(Int (Cl (C \/ B))) \/ (C \/ B) is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "/\" A) "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
the L_join of LattStr(# (T),(T),(T) #) . ((OL "/\" A),A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "/\" A),A] is set
{(OL "/\" A),A} is set
{(OL "/\" A)} is set
{{(OL "/\" A),A},{(OL "/\" A)}} is set
the L_join of LattStr(# (T),(T),(T) #) . [(OL "/\" A),A] is set
B is Element of (T)
C is Element of (T)
B /\ C is Element of bool the carrier of T
Int (B /\ C) is open Element of bool the carrier of T
Cl (Int (B /\ C)) is closed Element of bool the carrier of T
(Cl (Int (B /\ C))) /\ (B /\ C) is Element of bool the carrier of T
Cl C is closed Element of bool the carrier of T
Int (Cl C) is open Element of bool the carrier of T
A is Element of bool the carrier of T
((Cl (Int (B /\ C))) /\ (B /\ C)) \/ C is Element of bool the carrier of T
Cl (((Cl (Int (B /\ C))) /\ (B /\ C)) \/ C) is closed Element of bool the carrier of T
Int (Cl (((Cl (Int (B /\ C))) /\ (B /\ C)) \/ C)) is open Element of bool the carrier of T
(Int (Cl (((Cl (Int (B /\ C))) /\ (B /\ C)) \/ C))) \/ (((Cl (Int (B /\ C))) /\ (B /\ C)) \/ C) is Element of bool the carrier of T
(Int (Cl (((Cl (Int (B /\ C))) /\ (B /\ C)) \/ C))) \/ C is Element of bool the carrier of T
(Int (Cl C)) \/ C is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
B is Element of the carrier of LattStr(# (T),(T),(T) #)
A "\/" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (A,B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_join of LattStr(# (T),(T),(T) #) . [A,B] is set
OL "\/" (A "\/" B) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (OL,(A "\/" B)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(A "\/" B)] is set
{OL,(A "\/" B)} is set
{OL} is set
{{OL,(A "\/" B)},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,(A "\/" B)] is set
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "\/" A) "\/" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . ((OL "\/" A),B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "\/" A),B] is set
{(OL "\/" A),B} is set
{(OL "\/" A)} is set
{{(OL "\/" A),B},{(OL "\/" A)}} is set
the L_join of LattStr(# (T),(T),(T) #) . [(OL "\/" A),B] is set
C is Element of (T)
A is Element of (T)
C \/ A is Element of bool the carrier of T
Cl (C \/ A) is closed Element of bool the carrier of T
Int (Cl (C \/ A)) is open Element of bool the carrier of T
(Int (Cl (C \/ A))) \/ (C \/ A) is Element of bool the carrier of T
a is Element of (T)
A \/ a is Element of bool the carrier of T
Cl (A \/ a) is closed Element of bool the carrier of T
Int (Cl (A \/ a)) is open Element of bool the carrier of T
(Int (Cl (A \/ a))) \/ (A \/ a) is Element of bool the carrier of T
C \/ ((Int (Cl (A \/ a))) \/ (A \/ a)) is Element of bool the carrier of T
Cl (C \/ ((Int (Cl (A \/ a))) \/ (A \/ a))) is closed Element of bool the carrier of T
Int (Cl (C \/ ((Int (Cl (A \/ a))) \/ (A \/ a)))) is open Element of bool the carrier of T
(Int (Cl (C \/ ((Int (Cl (A \/ a))) \/ (A \/ a))))) \/ (C \/ ((Int (Cl (A \/ a))) \/ (A \/ a))) is Element of bool the carrier of T
C \/ (A \/ a) is Element of bool the carrier of T
Cl (C \/ (A \/ a)) is closed Element of bool the carrier of T
Int (Cl (C \/ (A \/ a))) is open Element of bool the carrier of T
(Int (Cl (C \/ (A \/ a)))) \/ (C \/ (A \/ a)) is Element of bool the carrier of T
(C \/ A) \/ a is Element of bool the carrier of T
(Int (Cl (C \/ (A \/ a)))) \/ ((C \/ A) \/ a) is Element of bool the carrier of T
Cl ((C \/ A) \/ a) is closed Element of bool the carrier of T
Int (Cl ((C \/ A) \/ a)) is open Element of bool the carrier of T
(Int (Cl ((C \/ A) \/ a))) \/ ((C \/ A) \/ a) is Element of bool the carrier of T
((Int (Cl (C \/ A))) \/ (C \/ A)) \/ a is Element of bool the carrier of T
Cl (((Int (Cl (C \/ A))) \/ (C \/ A)) \/ a) is closed Element of bool the carrier of T
Int (Cl (((Int (Cl (C \/ A))) \/ (C \/ A)) \/ a)) is open Element of bool the carrier of T
(Int (Cl (((Int (Cl (C \/ A))) \/ (C \/ A)) \/ a))) \/ (((Int (Cl (C \/ A))) \/ (C \/ A)) \/ a) is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
A "/\" OL is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (A,OL) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,OL] is set
{A,OL} is set
{A} is set
{{A,OL},{A}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [A,OL] is set
C is Element of (T)
B is Element of (T)
C /\ B is Element of bool the carrier of T
Int (C /\ B) is open Element of bool the carrier of T
Cl (Int (C /\ B)) is closed Element of bool the carrier of T
(Cl (Int (C /\ B))) /\ (C /\ B) is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
OL "/\" (OL "\/" A) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
the L_meet of LattStr(# (T),(T),(T) #) . (OL,(OL "\/" A)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(OL "\/" A)] is set
{OL,(OL "\/" A)} is set
{{OL,(OL "\/" A)},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,(OL "\/" A)] is set
B is Element of (T)
C is Element of (T)
B \/ C is Element of bool the carrier of T
Int B is open Element of bool the carrier of T
Cl (Int B) is closed Element of bool the carrier of T
A is Element of bool the carrier of T
Cl (B \/ C) is closed Element of bool the carrier of T
Int (Cl (B \/ C)) is open Element of bool the carrier of T
(Int (Cl (B \/ C))) \/ (B \/ C) is Element of bool the carrier of T
B /\ ((Int (Cl (B \/ C))) \/ (B \/ C)) is Element of bool the carrier of T
Int (B /\ ((Int (Cl (B \/ C))) \/ (B \/ C))) is open Element of bool the carrier of T
Cl (Int (B /\ ((Int (Cl (B \/ C))) \/ (B \/ C)))) is closed Element of bool the carrier of T
(Cl (Int (B /\ ((Int (Cl (B \/ C))) \/ (B \/ C))))) /\ (B /\ ((Int (Cl (B \/ C))) \/ (B \/ C))) is Element of bool the carrier of T
(Cl (Int (B /\ ((Int (Cl (B \/ C))) \/ (B \/ C))))) /\ B is Element of bool the carrier of T
(Cl (Int B)) /\ B is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
B is Element of the carrier of LattStr(# (T),(T),(T) #)
A "/\" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (A,B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [A,B] is set
OL "/\" (A "/\" B) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (OL,(A "/\" B)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(A "/\" B)] is set
{OL,(A "/\" B)} is set
{OL} is set
{{OL,(A "/\" B)},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,(A "/\" B)] is set
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "/\" A) "/\" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . ((OL "/\" A),B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "/\" A),B] is set
{(OL "/\" A),B} is set
{(OL "/\" A)} is set
{{(OL "/\" A),B},{(OL "/\" A)}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [(OL "/\" A),B] is set
C is Element of (T)
A is Element of (T)
C /\ A is Element of bool the carrier of T
Int (C /\ A) is open Element of bool the carrier of T
Cl (Int (C /\ A)) is closed Element of bool the carrier of T
(Cl (Int (C /\ A))) /\ (C /\ A) is Element of bool the carrier of T
a is Element of (T)
A /\ a is Element of bool the carrier of T
Int (A /\ a) is open Element of bool the carrier of T
Cl (Int (A /\ a)) is closed Element of bool the carrier of T
(Cl (Int (A /\ a))) /\ (A /\ a) is Element of bool the carrier of T
C /\ ((Cl (Int (A /\ a))) /\ (A /\ a)) is Element of bool the carrier of T
Int (C /\ ((Cl (Int (A /\ a))) /\ (A /\ a))) is open Element of bool the carrier of T
Cl (Int (C /\ ((Cl (Int (A /\ a))) /\ (A /\ a)))) is closed Element of bool the carrier of T
(Cl (Int (C /\ ((Cl (Int (A /\ a))) /\ (A /\ a))))) /\ (C /\ ((Cl (Int (A /\ a))) /\ (A /\ a))) is Element of bool the carrier of T
C /\ (A /\ a) is Element of bool the carrier of T
Int (C /\ (A /\ a)) is open Element of bool the carrier of T
Cl (Int (C /\ (A /\ a))) is closed Element of bool the carrier of T
(Cl (Int (C /\ (A /\ a)))) /\ (C /\ (A /\ a)) is Element of bool the carrier of T
(C /\ A) /\ a is Element of bool the carrier of T
(Cl (Int (C /\ (A /\ a)))) /\ ((C /\ A) /\ a) is Element of bool the carrier of T
Int ((C /\ A) /\ a) is open Element of bool the carrier of T
Cl (Int ((C /\ A) /\ a)) is closed Element of bool the carrier of T
(Cl (Int ((C /\ A) /\ a))) /\ ((C /\ A) /\ a) is Element of bool the carrier of T
((Cl (Int (C /\ A))) /\ (C /\ A)) /\ a is Element of bool the carrier of T
Int (((Cl (Int (C /\ A))) /\ (C /\ A)) /\ a) is open Element of bool the carrier of T
Cl (Int (((Cl (Int (C /\ A))) /\ (C /\ A)) /\ a)) is closed Element of bool the carrier of T
(Cl (Int (((Cl (Int (C /\ A))) /\ (C /\ A)) /\ a))) /\ (((Cl (Int (C /\ A))) /\ (C /\ A)) /\ a) is Element of bool the carrier of T
OL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
{} T is Element of bool the carrier of T
the carrier of OL is set
A is Element of the carrier of OL
B is Element of the carrier of OL
A "/\" B is Element of the carrier of OL
the L_meet of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
the L_meet of OL . (A,B) is Element of the carrier of OL
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_meet of OL . [A,B] is set
B "/\" A is Element of the carrier of OL
the L_meet of OL . (B,A) is Element of the carrier of OL
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
the L_meet of OL . [B,A] is set
C is Element of (T)
A is Element of (T)
C /\ A is Element of bool the carrier of T
A "/\" B is Element of the carrier of OL
Int C is open Element of bool the carrier of T
Cl (Int C) is closed Element of bool the carrier of T
(Cl (Int C)) /\ C is Element of bool the carrier of T
B "/\" A is Element of the carrier of OL
[#] T is open closed dense Element of bool the carrier of T
the carrier of OL is set
A is Element of the carrier of OL
B is Element of the carrier of OL
A "\/" B is Element of the carrier of OL
the L_join of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
the L_join of OL . (A,B) is Element of the carrier of OL
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_join of OL . [A,B] is set
B "\/" A is Element of the carrier of OL
the L_join of OL . (B,A) is Element of the carrier of OL
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
the L_join of OL . [B,A] is set
C is Element of (T)
A is Element of (T)
C \/ A is Element of bool the carrier of T
A "\/" B is Element of the carrier of OL
Cl C is closed Element of bool the carrier of T
Int (Cl C) is open Element of bool the carrier of T
(Int (Cl C)) \/ C is Element of bool the carrier of T
B "\/" A is Element of the carrier of OL
A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V86() LattStr
[#] T is open closed dense Element of bool the carrier of T
the carrier of A is set
C is Element of the carrier of A
A is Element of (T)
A ` is Element of bool the carrier of T
the carrier of T \ A is set
a is Element of bool the carrier of T
a is Element of the carrier of A
the L_meet of A is V1() V4([: the carrier of A, the carrier of A:]) V5( the carrier of A) Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[: the carrier of A, the carrier of A:] is V1() set
[:[: the carrier of A, the carrier of A:], the carrier of A:] is V1() set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
B is Element of the carrier of A
c is Element of the carrier of A
the L_meet of A . (B,c) is Element of the carrier of A
[B,c] is set
{B,c} is set
{B} is set
{{B,c},{B}} is set
the L_meet of A . [B,c] is set
v is Element of (T)
Int v is open Element of bool the carrier of T
Cl (Int v) is closed Element of bool the carrier of T
V is Element of bool the carrier of T
([#] T) /\ v is Element of bool the carrier of T
Int (([#] T) /\ v) is open Element of bool the carrier of T
Cl (Int (([#] T) /\ v)) is closed Element of bool the carrier of T
(Cl (Int (([#] T) /\ v))) /\ (([#] T) /\ v) is Element of bool the carrier of T
(Cl (Int (([#] T) /\ v))) /\ v is Element of bool the carrier of T
(Cl (Int v)) /\ v is Element of bool the carrier of T
a "\/" C is Element of the carrier of A
the L_join of A is V1() V4([: the carrier of A, the carrier of A:]) V5( the carrier of A) Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
the L_join of A . (a,C) is Element of the carrier of A
[a,C] is set
{a,C} is set
{a} is set
{{a,C},{a}} is set
the L_join of A . [a,C] is set
(A `) \/ A is Element of bool the carrier of T
Cl ((A `) \/ A) is closed Element of bool the carrier of T
Int (Cl ((A `) \/ A)) is open Element of bool the carrier of T
(Int (Cl ((A `) \/ A))) \/ ((A `) \/ A) is Element of bool the carrier of T
(Int (Cl ((A `) \/ A))) \/ ([#] T) is open Element of bool the carrier of T
Top A is Element of the carrier of A
C "\/" a is Element of the carrier of A
the L_join of A . (C,a) is Element of the carrier of A
[C,a] is set
{C,a} is set
{C} is set
{{C,a},{C}} is set
the L_join of A . [C,a] is set
a "/\" C is Element of the carrier of A
the L_meet of A . (a,C) is Element of the carrier of A
the L_meet of A . [a,C] is set
Bottom A is Element of the carrier of A
C "/\" a is Element of the carrier of A
the L_meet of A . (C,a) is Element of the carrier of A
the L_meet of A . [C,a] is set
C "\/" a is Element of the carrier of A
{} T is Element of bool the carrier of T
c is Element of the carrier of A
v is Element of the carrier of A
the L_join of A . (c,v) is Element of the carrier of A
[c,v] is set
{c,v} is set
{c} is set
{{c,v},{c}} is set
the L_join of A . [c,v] is set
V is Element of (T)
Cl V is closed Element of bool the carrier of T
Int (Cl V) is open Element of bool the carrier of T
E is Element of bool the carrier of T
({} T) \/ V is Element of bool the carrier of T
Cl (({} T) \/ V) is closed Element of bool the carrier of T
Int (Cl (({} T) \/ V)) is open Element of bool the carrier of T
(Int (Cl (({} T) \/ V))) \/ (({} T) \/ V) is Element of bool the carrier of T
([#] T) ` is open closed Element of bool the carrier of T
the carrier of T \ ([#] T) is set
(([#] T) `) \/ V is Element of bool the carrier of T
Cl ((([#] T) `) \/ V) is closed Element of bool the carrier of T
Int (Cl ((([#] T) `) \/ V)) is open Element of bool the carrier of T
(Int (Cl ((([#] T) `) \/ V))) \/ (({} T) \/ V) is Element of bool the carrier of T
V ` is Element of bool the carrier of T
the carrier of T \ V is set
(V `) ` is Element of bool the carrier of T
the carrier of T \ (V `) is set
(([#] T) `) \/ ((V `) `) is Element of bool the carrier of T
Cl ((([#] T) `) \/ ((V `) `)) is closed Element of bool the carrier of T
Int (Cl ((([#] T) `) \/ ((V `) `))) is open Element of bool the carrier of T
(Int (Cl ((([#] T) `) \/ ((V `) `)))) \/ ((([#] T) `) \/ V) is Element of bool the carrier of T
([#] T) /\ (V `) is Element of bool the carrier of T
(([#] T) /\ (V `)) ` is Element of bool the carrier of T
the carrier of T \ (([#] T) /\ (V `)) is set
Cl ((([#] T) /\ (V `)) `) is closed Element of bool the carrier of T
Int (Cl ((([#] T) /\ (V `)) `)) is open Element of bool the carrier of T
(Int (Cl ((([#] T) /\ (V `)) `))) \/ ((([#] T) `) \/ ((V `) `)) is Element of bool the carrier of T
(Int (Cl ((([#] T) /\ (V `)) `))) \/ ((([#] T) /\ (V `)) `) is Element of bool the carrier of T
Cl ((V `) `) is closed Element of bool the carrier of T
Int (Cl ((V `) `)) is open Element of bool the carrier of T
(Int (Cl ((V `) `))) \/ ((([#] T) /\ (V `)) `) is Element of bool the carrier of T
(Int (Cl V)) \/ ((V `) `) is Element of bool the carrier of T
a "/\" C is Element of the carrier of A
(A `) /\ A is Element of bool the carrier of T
Int ((A `) /\ A) is open Element of bool the carrier of T
Cl (Int ((A `) /\ A)) is closed Element of bool the carrier of T
(Cl (Int ((A `) /\ A))) /\ ((A `) /\ A) is Element of bool the carrier of T
(Cl (Int ((A `) /\ A))) /\ ({} T) is Element of bool the carrier of T
C "/\" a is Element of the carrier of A
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
bool (bool the carrier of T) is non empty set
OL is set
A is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
{} T is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
OL is Element of [:(T),(T):]
OL `1 is Element of (T)
OL `2 is Element of (T)
A is Element of (T)
C is Element of bool the carrier of T
B is Element of (T)
A is Element of bool the carrier of T
C \/ A is Element of bool the carrier of T
A \/ B is Element of bool the carrier of T
a is Element of (T)
c is Element of (T)
v is Element of (T)
[c,v] is Element of [:(T),(T):]
{c,v} is set
{c} is set
{{c,v},{c}} is set
c \/ v is Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
OL . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL . [A,B] is set
A \/ B is Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
OL . [A,B] is Element of (T)
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
(T) is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
L is Element of (T)
OL is Element of (T)
(T) . (L,OL) is Element of (T)
[L,OL] is set
{L,OL} is set
{L} is set
{{L,OL},{L}} is set
(T) . [L,OL] is set
(T) . (L,OL) is set
(T) . [L,OL] is set
C is Element of bool the carrier of T
A is Element of bool the carrier of T
A \/ C is Element of bool the carrier of T
L \/ OL is Element of bool the carrier of T
Cl (L \/ OL) is closed Element of bool the carrier of T
Int (Cl (L \/ OL)) is open Element of bool the carrier of T
A is Element of (T)
B is Element of (T)
A \/ B is Element of bool the carrier of T
Cl (A \/ B) is closed Element of bool the carrier of T
Int (Cl (A \/ B)) is open Element of bool the carrier of T
(Int (Cl (A \/ B))) \/ (A \/ B) is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
OL is Element of [:(T),(T):]
OL `1 is Element of (T)
OL `2 is Element of (T)
A is Element of (T)
B is Element of (T)
A /\ B is Element of bool the carrier of T
Int (A /\ B) is open Element of bool the carrier of T
Cl (Int (A /\ B)) is closed Element of bool the carrier of T
C is Element of (T)
A is Element of (T)
a is Element of (T)
[A,a] is Element of [:(T),(T):]
{A,a} is set
{A} is set
{{A,a},{A}} is set
A /\ a is Element of bool the carrier of T
Int (A /\ a) is open Element of bool the carrier of T
Cl (Int (A /\ a)) is closed Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
OL . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL . [A,B] is set
A /\ B is Element of bool the carrier of T
Int (A /\ B) is open Element of bool the carrier of T
Cl (Int (A /\ B)) is closed Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
OL . [A,B] is Element of (T)
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
(T) is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
L is Element of (T)
OL is Element of (T)
(T) . (L,OL) is Element of (T)
[L,OL] is set
{L,OL} is set
{L} is set
{{L,OL},{L}} is set
(T) . [L,OL] is set
(T) . (L,OL) is set
(T) . [L,OL] is set
A is Element of bool the carrier of T
L /\ OL is Element of bool the carrier of T
Int (L /\ OL) is open Element of bool the carrier of T
A is Element of bool the carrier of T
A /\ A is Element of bool the carrier of T
Cl (A /\ A) is closed Element of bool the carrier of T
Cl (Int (L /\ OL)) is closed Element of bool the carrier of T
B is Element of (T)
C is Element of (T)
B /\ C is Element of bool the carrier of T
Int (B /\ C) is open Element of bool the carrier of T
Cl (Int (B /\ C)) is closed Element of bool the carrier of T
(Cl (Int (B /\ C))) /\ (B /\ C) is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
A "\/" OL is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (A,OL) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,OL] is set
{A,OL} is set
{A} is set
{{A,OL},{A}} is set
the L_join of LattStr(# (T),(T),(T) #) . [A,OL] is set
C is Element of (T)
B is Element of (T)
C \/ B is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "/\" A) "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
the L_join of LattStr(# (T),(T),(T) #) . ((OL "/\" A),A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "/\" A),A] is set
{(OL "/\" A),A} is set
{(OL "/\" A)} is set
{{(OL "/\" A),A},{(OL "/\" A)}} is set
the L_join of LattStr(# (T),(T),(T) #) . [(OL "/\" A),A] is set
B is Element of (T)
Int B is open Element of bool the carrier of T
Cl (Int B) is closed Element of bool the carrier of T
C is Element of (T)
(Cl (Int B)) /\ C is Element of bool the carrier of T
Int C is open Element of bool the carrier of T
Cl (Int C) is closed Element of bool the carrier of T
A is Element of bool the carrier of T
B /\ C is Element of bool the carrier of T
Int (B /\ C) is open Element of bool the carrier of T
Cl (Int (B /\ C)) is closed Element of bool the carrier of T
(Int B) /\ (Int C) is open Element of bool the carrier of T
Cl ((Int B) /\ (Int C)) is closed Element of bool the carrier of T
(Cl (Int (B /\ C))) \/ C is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
OL "/\" (OL "\/" A) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
the L_meet of LattStr(# (T),(T),(T) #) . (OL,(OL "\/" A)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(OL "\/" A)] is set
{OL,(OL "\/" A)} is set
{{OL,(OL "\/" A)},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,(OL "\/" A)] is set
B is Element of (T)
C is Element of (T)
B \/ C is Element of bool the carrier of T
B /\ (B \/ C) is Element of bool the carrier of T
Int (B /\ (B \/ C)) is open Element of bool the carrier of T
Cl (Int (B /\ (B \/ C))) is closed Element of bool the carrier of T
Int B is open Element of bool the carrier of T
Cl (Int B) is closed Element of bool the carrier of T
A is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
B is Element of the carrier of LattStr(# (T),(T),(T) #)
A "\/" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (A,B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_join of LattStr(# (T),(T),(T) #) . [A,B] is set
OL "\/" (A "\/" B) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (OL,(A "\/" B)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(A "\/" B)] is set
{OL,(A "\/" B)} is set
{OL} is set
{{OL,(A "\/" B)},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,(A "\/" B)] is set
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "\/" A) "\/" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . ((OL "\/" A),B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "\/" A),B] is set
{(OL "\/" A),B} is set
{(OL "\/" A)} is set
{{(OL "\/" A),B},{(OL "\/" A)}} is set
the L_join of LattStr(# (T),(T),(T) #) . [(OL "\/" A),B] is set
C is Element of (T)
A is Element of (T)
C \/ A is Element of bool the carrier of T
a is Element of (T)
A \/ a is Element of bool the carrier of T
C \/ (A \/ a) is Element of bool the carrier of T
(C \/ A) \/ a is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
B is Element of the carrier of LattStr(# (T),(T),(T) #)
A "/\" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (A,B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [A,B] is set
OL "/\" (A "/\" B) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (OL,(A "/\" B)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(A "/\" B)] is set
{OL,(A "/\" B)} is set
{OL} is set
{{OL,(A "/\" B)},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,(A "/\" B)] is set
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "/\" A) "/\" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . ((OL "/\" A),B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "/\" A),B] is set
{(OL "/\" A),B} is set
{(OL "/\" A)} is set
{{(OL "/\" A),B},{(OL "/\" A)}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [(OL "/\" A),B] is set
C is Element of (T)
A is Element of (T)
a is Element of (T)
C /\ A is Element of bool the carrier of T
Int (C /\ A) is open Element of bool the carrier of T
Cl (Int (C /\ A)) is closed Element of bool the carrier of T
A /\ a is Element of bool the carrier of T
Int (A /\ a) is open Element of bool the carrier of T
Cl (Int (A /\ a)) is closed Element of bool the carrier of T
C /\ (Cl (Int (A /\ a))) is Element of bool the carrier of T
Int (C /\ (Cl (Int (A /\ a)))) is open Element of bool the carrier of T
Cl (Int (C /\ (Cl (Int (A /\ a))))) is closed Element of bool the carrier of T
(Cl (Int (C /\ A))) /\ a is Element of bool the carrier of T
Int ((Cl (Int (C /\ A))) /\ a) is open Element of bool the carrier of T
Cl (Int ((Cl (Int (C /\ A))) /\ a)) is closed Element of bool the carrier of T
c is Element of bool the carrier of T
v is Element of bool the carrier of T
V is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
A "/\" OL is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (A,OL) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,OL] is set
{A,OL} is set
{A} is set
{{A,OL},{A}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [A,OL] is set
C is Element of (T)
B is Element of (T)
C /\ B is Element of bool the carrier of T
Int (C /\ B) is open Element of bool the carrier of T
Cl (Int (C /\ B)) is closed Element of bool the carrier of T
OL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
[#] T is open closed dense Element of bool the carrier of T
the carrier of OL is set
A is Element of the carrier of OL
B is Element of the carrier of OL
A "\/" B is Element of the carrier of OL
the L_join of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
the L_join of OL . (A,B) is Element of the carrier of OL
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_join of OL . [A,B] is set
B "\/" A is Element of the carrier of OL
the L_join of OL . (B,A) is Element of the carrier of OL
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
the L_join of OL . [B,A] is set
A "\/" B is Element of the carrier of OL
C is Element of (T)
A is Element of (T)
C \/ A is Element of bool the carrier of T
B "\/" A is Element of the carrier of OL
the carrier of OL is set
A is Element of the carrier of OL
B is Element of the carrier of OL
C is Element of the carrier of OL
B "\/" C is Element of the carrier of OL
the L_join of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
the L_join of OL . (B,C) is Element of the carrier of OL
[B,C] is set
{B,C} is set
{B} is set
{{B,C},{B}} is set
the L_join of OL . [B,C] is set
A "/\" (B "\/" C) is Element of the carrier of OL
the L_meet of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
the L_meet of OL . (A,(B "\/" C)) is Element of the carrier of OL
[A,(B "\/" C)] is set
{A,(B "\/" C)} is set
{A} is set
{{A,(B "\/" C)},{A}} is set
the L_meet of OL . [A,(B "\/" C)] is set
A "/\" B is Element of the carrier of OL
the L_meet of OL . (A,B) is Element of the carrier of OL
[A,B] is set
{A,B} is set
{{A,B},{A}} is set
the L_meet of OL . [A,B] is set
A "/\" C is Element of the carrier of OL
the L_meet of OL . (A,C) is Element of the carrier of OL
[A,C] is set
{A,C} is set
{{A,C},{A}} is set
the L_meet of OL . [A,C] is set
(A "/\" B) "\/" (A "/\" C) is Element of the carrier of OL
the L_join of OL . ((A "/\" B),(A "/\" C)) is Element of the carrier of OL
[(A "/\" B),(A "/\" C)] is set
{(A "/\" B),(A "/\" C)} is set
{(A "/\" B)} is set
{{(A "/\" B),(A "/\" C)},{(A "/\" B)}} is set
the L_join of OL . [(A "/\" B),(A "/\" C)] is set
A is Element of (T)
v is Element of bool the carrier of T
a is Element of (T)
V is Element of bool the carrier of T
A "/\" C is Element of the carrier of OL
c is Element of (T)
A /\ c is Element of bool the carrier of T
Int (A /\ c) is open Element of bool the carrier of T
Cl (Int (A /\ c)) is closed Element of bool the carrier of T
A "/\" B is Element of the carrier of OL
A /\ a is Element of bool the carrier of T
Int (A /\ a) is open Element of bool the carrier of T
Cl (Int (A /\ a)) is closed Element of bool the carrier of T
B "\/" C is Element of the carrier of OL
a \/ c is Element of bool the carrier of T
A "/\" (B "\/" C) is Element of the carrier of OL
the L_meet of OL . (A,(B "\/" C)) is Element of the carrier of OL
[A,(B "\/" C)] is set
{A,(B "\/" C)} is set
{{A,(B "\/" C)},{A}} is set
the L_meet of OL . [A,(B "\/" C)] is set
A /\ (a \/ c) is Element of bool the carrier of T
Int (A /\ (a \/ c)) is open Element of bool the carrier of T
Cl (Int (A /\ (a \/ c))) is closed Element of bool the carrier of T
(A /\ a) \/ (A /\ c) is Element of bool the carrier of T
Int ((A /\ a) \/ (A /\ c)) is open Element of bool the carrier of T
Cl (Int ((A /\ a) \/ (A /\ c))) is closed Element of bool the carrier of T
(Cl (Int (A /\ a))) \/ (Cl (Int (A /\ c))) is closed Element of bool the carrier of T
(A "/\" B) "\/" (A "/\" C) is Element of the carrier of OL
the L_join of OL . ((A "/\" B),(A "/\" C)) is Element of the carrier of OL
[(A "/\" B),(A "/\" C)] is set
{(A "/\" B),(A "/\" C)} is set
{(A "/\" B)} is set
{{(A "/\" B),(A "/\" C)},{(A "/\" B)}} is set
the L_join of OL . [(A "/\" B),(A "/\" C)] is set
[#] T is open closed dense Element of bool the carrier of T
the carrier of OL is set
B is Element of the carrier of OL
C is Element of (T)
A is Element of bool the carrier of T
C ` is Element of bool the carrier of T
the carrier of T \ C is set
Cl (C `) is closed Element of bool the carrier of T
a is Element of the carrier of OL
the L_meet of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
A is Element of the carrier of OL
c is Element of the carrier of OL
the L_meet of OL . (A,c) is Element of the carrier of OL
[A,c] is set
{A,c} is set
{A} is set
{{A,c},{A}} is set
the L_meet of OL . [A,c] is set
v is Element of (T)
([#] T) /\ v is Element of bool the carrier of T
Int (([#] T) /\ v) is open Element of bool the carrier of T
Cl (Int (([#] T) /\ v)) is closed Element of bool the carrier of T
Int v is open Element of bool the carrier of T
Cl (Int v) is closed Element of bool the carrier of T
V is Element of bool the carrier of T
a "\/" B is Element of the carrier of OL
the L_join of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
the L_join of OL . (a,B) is Element of the carrier of OL
[a,B] is set
{a,B} is set
{a} is set
{{a,B},{a}} is set
the L_join of OL . [a,B] is set
(Cl (C `)) \/ C is Element of bool the carrier of T
A ` is Element of bool the carrier of T
the carrier of T \ A is set
Cl (A `) is closed Element of bool the carrier of T
Cl A is closed Element of bool the carrier of T
(Cl (A `)) \/ (Cl A) is closed Element of bool the carrier of T
(C `) \/ C is Element of bool the carrier of T
Cl ((C `) \/ C) is closed Element of bool the carrier of T
Cl ([#] T) is closed Element of bool the carrier of T
Top OL is Element of the carrier of OL
B "\/" a is Element of the carrier of OL
the L_join of OL . (B,a) is Element of the carrier of OL
[B,a] is set
{B,a} is set
{B} is set
{{B,a},{B}} is set
the L_join of OL . [B,a] is set
a "/\" B is Element of the carrier of OL
the L_meet of OL . (a,B) is Element of the carrier of OL
the L_meet of OL . [a,B] is set
Bottom OL is Element of the carrier of OL
B "/\" a is Element of the carrier of OL
the L_meet of OL . (B,a) is Element of the carrier of OL
the L_meet of OL . [B,a] is set
B "\/" a is Element of the carrier of OL
{} T is Element of bool the carrier of T
c is Element of the carrier of OL
v is Element of the carrier of OL
the L_join of OL . (c,v) is Element of the carrier of OL
[c,v] is set
{c,v} is set
{c} is set
{{c,v},{c}} is set
the L_join of OL . [c,v] is set
V is Element of (T)
({} T) \/ V is Element of bool the carrier of T
([#] T) ` is open closed Element of bool the carrier of T
the carrier of T \ ([#] T) is set
V ` is Element of bool the carrier of T
the carrier of T \ V is set
(V `) ` is Element of bool the carrier of T
the carrier of T \ (V `) is set
(([#] T) `) \/ ((V `) `) is Element of bool the carrier of T
([#] T) /\ (V `) is Element of bool the carrier of T
(([#] T) /\ (V `)) ` is Element of bool the carrier of T
the carrier of T \ (([#] T) /\ (V `)) is set
a "/\" B is Element of the carrier of OL
C /\ (Cl (C `)) is Element of bool the carrier of T
Int (C /\ (Cl (C `))) is open Element of bool the carrier of T
Cl (Int (C /\ (Cl (C `)))) is closed Element of bool the carrier of T
Cl ({} T) is closed Element of bool the carrier of T
B "/\" a is Element of the carrier of OL
{} T is Element of bool the carrier of T
the carrier of OL is set
A is Element of the carrier of OL
B is Element of the carrier of OL
A "/\" B is Element of the carrier of OL
the L_meet of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
the L_meet of OL . (A,B) is Element of the carrier of OL
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_meet of OL . [A,B] is set
B "/\" A is Element of the carrier of OL
the L_meet of OL . (B,A) is Element of the carrier of OL
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
the L_meet of OL . [B,A] is set
A "/\" B is Element of the carrier of OL
C is Element of (T)
A is Element of (T)
C /\ A is Element of bool the carrier of T
Int (C /\ A) is open Element of bool the carrier of T
Cl (Int (C /\ A)) is closed Element of bool the carrier of T
B "/\" A is Element of the carrier of OL
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
bool (bool the carrier of T) is non empty set
OL is set
A is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
{} T is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
OL is Element of [:(T),(T):]
OL `1 is Element of (T)
OL `2 is Element of (T)
A is Element of (T)
B is Element of (T)
A \/ B is Element of bool the carrier of T
Cl (A \/ B) is closed Element of bool the carrier of T
Int (Cl (A \/ B)) is open Element of bool the carrier of T
C is Element of (T)
A is Element of (T)
a is Element of (T)
[A,a] is Element of [:(T),(T):]
{A,a} is set
{A} is set
{{A,a},{A}} is set
A \/ a is Element of bool the carrier of T
Cl (A \/ a) is closed Element of bool the carrier of T
Int (Cl (A \/ a)) is open Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
OL . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL . [A,B] is set
A \/ B is Element of bool the carrier of T
Cl (A \/ B) is closed Element of bool the carrier of T
Int (Cl (A \/ B)) is open Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
OL . [A,B] is Element of (T)
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
(T) is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
L is Element of (T)
OL is Element of (T)
(T) . (L,OL) is Element of (T)
[L,OL] is set
{L,OL} is set
{L} is set
{{L,OL},{L}} is set
(T) . [L,OL] is set
(T) . (L,OL) is set
(T) . [L,OL] is set
A is Element of bool the carrier of T
L \/ OL is Element of bool the carrier of T
Cl (L \/ OL) is closed Element of bool the carrier of T
A is Element of bool the carrier of T
A \/ A is Element of bool the carrier of T
Int (A \/ A) is open Element of bool the carrier of T
Int (Cl (L \/ OL)) is open Element of bool the carrier of T
B is Element of (T)
C is Element of (T)
B \/ C is Element of bool the carrier of T
Cl (B \/ C) is closed Element of bool the carrier of T
Int (Cl (B \/ C)) is open Element of bool the carrier of T
(Int (Cl (B \/ C))) \/ (B \/ C) is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
OL is Element of [:(T),(T):]
OL `1 is Element of (T)
OL `2 is Element of (T)
A is Element of (T)
C is Element of bool the carrier of T
B is Element of (T)
A is Element of bool the carrier of T
C /\ A is Element of bool the carrier of T
A /\ B is Element of bool the carrier of T
a is Element of (T)
c is Element of (T)
v is Element of (T)
[c,v] is Element of [:(T),(T):]
{c,v} is set
{c} is set
{{c,v},{c}} is set
c /\ v is Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
OL . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
OL . [A,B] is set
A /\ B is Element of bool the carrier of T
[A,B] is Element of [:(T),(T):]
OL . [A,B] is Element of (T)
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
(T) is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
L is Element of (T)
OL is Element of (T)
(T) . (L,OL) is Element of (T)
[L,OL] is set
{L,OL} is set
{L} is set
{{L,OL},{L}} is set
(T) . [L,OL] is set
(T) . (L,OL) is set
(T) . [L,OL] is set
C is Element of bool the carrier of T
A is Element of bool the carrier of T
A /\ C is Element of bool the carrier of T
L /\ OL is Element of bool the carrier of T
Int (L /\ OL) is open Element of bool the carrier of T
Cl (Int (L /\ OL)) is closed Element of bool the carrier of T
A is Element of (T)
B is Element of (T)
A /\ B is Element of bool the carrier of T
Int (A /\ B) is open Element of bool the carrier of T
Cl (Int (A /\ B)) is closed Element of bool the carrier of T
(Cl (Int (A /\ B))) /\ (A /\ B) is Element of bool the carrier of T
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
A "\/" OL is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (A,OL) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,OL] is set
{A,OL} is set
{A} is set
{{A,OL},{A}} is set
the L_join of LattStr(# (T),(T),(T) #) . [A,OL] is set
C is Element of (T)
B is Element of (T)
C \/ B is Element of bool the carrier of T
Cl (C \/ B) is closed Element of bool the carrier of T
Int (Cl (C \/ B)) is open Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "/\" A) "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
the L_join of LattStr(# (T),(T),(T) #) . ((OL "/\" A),A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "/\" A),A] is set
{(OL "/\" A),A} is set
{(OL "/\" A)} is set
{{(OL "/\" A),A},{(OL "/\" A)}} is set
the L_join of LattStr(# (T),(T),(T) #) . [(OL "/\" A),A] is set
C is Element of (T)
B is Element of (T)
B /\ C is Element of bool the carrier of T
(B /\ C) \/ C is Element of bool the carrier of T
Cl ((B /\ C) \/ C) is closed Element of bool the carrier of T
Int (Cl ((B /\ C) \/ C)) is open Element of bool the carrier of T
Cl C is closed Element of bool the carrier of T
Int (Cl C) is open Element of bool the carrier of T
A is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
OL "/\" (OL "\/" A) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
the L_meet of LattStr(# (T),(T),(T) #) . (OL,(OL "\/" A)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(OL "\/" A)] is set
{OL,(OL "\/" A)} is set
{{OL,(OL "\/" A)},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,(OL "\/" A)] is set
B is Element of (T)
C is Element of (T)
Cl C is closed Element of bool the carrier of T
Int (Cl C) is open Element of bool the carrier of T
B \/ (Int (Cl C)) is Element of bool the carrier of T
Cl B is closed Element of bool the carrier of T
Int (Cl B) is open Element of bool the carrier of T
A is Element of bool the carrier of T
(Cl B) \/ (Cl C) is closed Element of bool the carrier of T
Int ((Cl B) \/ (Cl C)) is open Element of bool the carrier of T
B \/ C is Element of bool the carrier of T
Cl (B \/ C) is closed Element of bool the carrier of T
Int (Cl (B \/ C)) is open Element of bool the carrier of T
B /\ (Int (Cl (B \/ C))) is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
B is Element of the carrier of LattStr(# (T),(T),(T) #)
A "/\" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (A,B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [A,B] is set
OL "/\" (A "/\" B) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (OL,(A "/\" B)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(A "/\" B)] is set
{OL,(A "/\" B)} is set
{OL} is set
{{OL,(A "/\" B)},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,(A "/\" B)] is set
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "/\" A) "/\" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . ((OL "/\" A),B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "/\" A),B] is set
{(OL "/\" A),B} is set
{(OL "/\" A)} is set
{{(OL "/\" A),B},{(OL "/\" A)}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [(OL "/\" A),B] is set
C is Element of (T)
A is Element of (T)
C /\ A is Element of bool the carrier of T
a is Element of (T)
A /\ a is Element of bool the carrier of T
C /\ (A /\ a) is Element of bool the carrier of T
(C /\ A) /\ a is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
B is Element of the carrier of LattStr(# (T),(T),(T) #)
A "\/" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_join of LattStr(# (T),(T),(T) #) . (A,B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_join of LattStr(# (T),(T),(T) #) . [A,B] is set
OL "\/" (A "\/" B) is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (OL,(A "\/" B)) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,(A "\/" B)] is set
{OL,(A "\/" B)} is set
{OL} is set
{{OL,(A "\/" B)},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,(A "\/" B)] is set
OL "\/" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{{OL,A},{OL}} is set
the L_join of LattStr(# (T),(T),(T) #) . [OL,A] is set
(OL "\/" A) "\/" B is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_join of LattStr(# (T),(T),(T) #) . ((OL "\/" A),B) is Element of the carrier of LattStr(# (T),(T),(T) #)
[(OL "\/" A),B] is set
{(OL "\/" A),B} is set
{(OL "\/" A)} is set
{{(OL "\/" A),B},{(OL "\/" A)}} is set
the L_join of LattStr(# (T),(T),(T) #) . [(OL "\/" A),B] is set
C is Element of (T)
A is Element of (T)
a is Element of (T)
C \/ A is Element of bool the carrier of T
Cl (C \/ A) is closed Element of bool the carrier of T
Int (Cl (C \/ A)) is open Element of bool the carrier of T
A \/ a is Element of bool the carrier of T
Cl (A \/ a) is closed Element of bool the carrier of T
Int (Cl (A \/ a)) is open Element of bool the carrier of T
C \/ (Int (Cl (A \/ a))) is Element of bool the carrier of T
Cl (C \/ (Int (Cl (A \/ a)))) is closed Element of bool the carrier of T
Int (Cl (C \/ (Int (Cl (A \/ a))))) is open Element of bool the carrier of T
(Int (Cl (C \/ A))) \/ a is Element of bool the carrier of T
Cl ((Int (Cl (C \/ A))) \/ a) is closed Element of bool the carrier of T
Int (Cl ((Int (Cl (C \/ A))) \/ a)) is open Element of bool the carrier of T
c is Element of bool the carrier of T
v is Element of bool the carrier of T
V is Element of bool the carrier of T
the carrier of LattStr(# (T),(T),(T) #) is set
OL is Element of the carrier of LattStr(# (T),(T),(T) #)
A is Element of the carrier of LattStr(# (T),(T),(T) #)
OL "/\" A is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) is V1() V4([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):]) V5( the carrier of LattStr(# (T),(T),(T) #)) Function-like V18([: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #)) Element of bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):]
[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):] is V1() set
[:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is V1() set
bool [:[: the carrier of LattStr(# (T),(T),(T) #), the carrier of LattStr(# (T),(T),(T) #):], the carrier of LattStr(# (T),(T),(T) #):] is non empty set
the L_meet of LattStr(# (T),(T),(T) #) . (OL,A) is Element of the carrier of LattStr(# (T),(T),(T) #)
[OL,A] is set
{OL,A} is set
{OL} is set
{{OL,A},{OL}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [OL,A] is set
A "/\" OL is Element of the carrier of LattStr(# (T),(T),(T) #)
the L_meet of LattStr(# (T),(T),(T) #) . (A,OL) is Element of the carrier of LattStr(# (T),(T),(T) #)
[A,OL] is set
{A,OL} is set
{A} is set
{{A,OL},{A}} is set
the L_meet of LattStr(# (T),(T),(T) #) . [A,OL] is set
C is Element of (T)
B is Element of (T)
C /\ B is Element of bool the carrier of T
OL is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
[#] T is open closed dense Element of bool the carrier of T
the carrier of OL is set
A is Element of the carrier of OL
B is Element of the carrier of OL
A "\/" B is Element of the carrier of OL
the L_join of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
the L_join of OL . (A,B) is Element of the carrier of OL
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_join of OL . [A,B] is set
B "\/" A is Element of the carrier of OL
the L_join of OL . (B,A) is Element of the carrier of OL
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
the L_join of OL . [B,A] is set
A "\/" B is Element of the carrier of OL
C is Element of (T)
A is Element of (T)
C \/ A is Element of bool the carrier of T
Cl (C \/ A) is closed Element of bool the carrier of T
Int (Cl (C \/ A)) is open Element of bool the carrier of T
Cl C is closed Element of bool the carrier of T
Int (Cl C) is open Element of bool the carrier of T
B "\/" A is Element of the carrier of OL
the carrier of OL is set
A is Element of the carrier of OL
B is Element of the carrier of OL
C is Element of the carrier of OL
B "\/" C is Element of the carrier of OL
the L_join of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
the L_join of OL . (B,C) is Element of the carrier of OL
[B,C] is set
{B,C} is set
{B} is set
{{B,C},{B}} is set
the L_join of OL . [B,C] is set
A "/\" (B "\/" C) is Element of the carrier of OL
the L_meet of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
the L_meet of OL . (A,(B "\/" C)) is Element of the carrier of OL
[A,(B "\/" C)] is set
{A,(B "\/" C)} is set
{A} is set
{{A,(B "\/" C)},{A}} is set
the L_meet of OL . [A,(B "\/" C)] is set
A "/\" B is Element of the carrier of OL
the L_meet of OL . (A,B) is Element of the carrier of OL
[A,B] is set
{A,B} is set
{{A,B},{A}} is set
the L_meet of OL . [A,B] is set
A "/\" C is Element of the carrier of OL
the L_meet of OL . (A,C) is Element of the carrier of OL
[A,C] is set
{A,C} is set
{{A,C},{A}} is set
the L_meet of OL . [A,C] is set
(A "/\" B) "\/" (A "/\" C) is Element of the carrier of OL
the L_join of OL . ((A "/\" B),(A "/\" C)) is Element of the carrier of OL
[(A "/\" B),(A "/\" C)] is set
{(A "/\" B),(A "/\" C)} is set
{(A "/\" B)} is set
{{(A "/\" B),(A "/\" C)},{(A "/\" B)}} is set
the L_join of OL . [(A "/\" B),(A "/\" C)] is set
A is Element of (T)
v is Element of bool the carrier of T
A "/\" C is Element of the carrier of OL
c is Element of (T)
A /\ c is Element of bool the carrier of T
V is Element of bool the carrier of T
a is Element of (T)
E is Element of bool the carrier of T
A "/\" B is Element of the carrier of OL
A /\ a is Element of bool the carrier of T
B "\/" C is Element of the carrier of OL
a \/ c is Element of bool the carrier of T
Cl (a \/ c) is closed Element of bool the carrier of T
Int (Cl (a \/ c)) is open Element of bool the carrier of T
A "/\" (B "\/" C) is Element of the carrier of OL
the L_meet of OL . (A,(B "\/" C)) is Element of the carrier of OL
[A,(B "\/" C)] is set
{A,(B "\/" C)} is set
{{A,(B "\/" C)},{A}} is set
the L_meet of OL . [A,(B "\/" C)] is set
A /\ (Int (Cl (a \/ c))) is Element of bool the carrier of T
Cl A is closed Element of bool the carrier of T
Int (Cl A) is open Element of bool the carrier of T
(Int (Cl A)) /\ (Int (Cl (a \/ c))) is open Element of bool the carrier of T
E \/ V is Element of bool the carrier of T
v /\ (E \/ V) is Element of bool the carrier of T
Cl (v /\ (E \/ V)) is closed Element of bool the carrier of T
Int (Cl (v /\ (E \/ V))) is open Element of bool the carrier of T
(A /\ a) \/ (A /\ c) is Element of bool the carrier of T
Cl ((A /\ a) \/ (A /\ c)) is closed Element of bool the carrier of T
Int (Cl ((A /\ a) \/ (A /\ c))) is open Element of bool the carrier of T
(A "/\" B) "\/" (A "/\" C) is Element of the carrier of OL
the L_join of OL . ((A "/\" B),(A "/\" C)) is Element of the carrier of OL
[(A "/\" B),(A "/\" C)] is set
{(A "/\" B),(A "/\" C)} is set
{(A "/\" B)} is set
{{(A "/\" B),(A "/\" C)},{(A "/\" B)}} is set
the L_join of OL . [(A "/\" B),(A "/\" C)] is set
[#] T is open closed dense Element of bool the carrier of T
the carrier of OL is set
B is Element of the carrier of OL
C is Element of (T)
A is Element of bool the carrier of T
C ` is Element of bool the carrier of T
the carrier of T \ C is set
Int (C `) is open Element of bool the carrier of T
a is Element of the carrier of OL
the L_meet of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
A is Element of the carrier of OL
c is Element of the carrier of OL
the L_meet of OL . (A,c) is Element of the carrier of OL
[A,c] is set
{A,c} is set
{A} is set
{{A,c},{A}} is set
the L_meet of OL . [A,c] is set
v is Element of (T)
([#] T) /\ v is Element of bool the carrier of T
a "\/" B is Element of the carrier of OL
the L_join of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
the L_join of OL . (a,B) is Element of the carrier of OL
[a,B] is set
{a,B} is set
{a} is set
{{a,B},{a}} is set
the L_join of OL . [a,B] is set
C \/ (Int (C `)) is Element of bool the carrier of T
Cl (C \/ (Int (C `))) is closed Element of bool the carrier of T
Int (Cl (C \/ (Int (C `)))) is open Element of bool the carrier of T
Int ([#] T) is open Element of bool the carrier of T
Top OL is Element of the carrier of OL
B "\/" a is Element of the carrier of OL
the L_join of OL . (B,a) is Element of the carrier of OL
[B,a] is set
{B,a} is set
{B} is set
{{B,a},{B}} is set
the L_join of OL . [B,a] is set
a "/\" B is Element of the carrier of OL
the L_meet of OL . (a,B) is Element of the carrier of OL
the L_meet of OL . [a,B] is set
Bottom OL is Element of the carrier of OL
B "/\" a is Element of the carrier of OL
the L_meet of OL . (B,a) is Element of the carrier of OL
the L_meet of OL . [B,a] is set
B "\/" a is Element of the carrier of OL
{} T is Element of bool the carrier of T
c is Element of the carrier of OL
v is Element of the carrier of OL
the L_join of OL . (c,v) is Element of the carrier of OL
[c,v] is set
{c,v} is set
{c} is set
{{c,v},{c}} is set
the L_join of OL . [c,v] is set
V is Element of (T)
({} T) \/ V is Element of bool the carrier of T
Cl (({} T) \/ V) is closed Element of bool the carrier of T
Int (Cl (({} T) \/ V)) is open Element of bool the carrier of T
([#] T) ` is open closed Element of bool the carrier of T
the carrier of T \ ([#] T) is set
V ` is Element of bool the carrier of T
the carrier of T \ V is set
(V `) ` is Element of bool the carrier of T
the carrier of T \ (V `) is set
(([#] T) `) \/ ((V `) `) is Element of bool the carrier of T
Cl ((([#] T) `) \/ ((V `) `)) is closed Element of bool the carrier of T
Int (Cl ((([#] T) `) \/ ((V `) `))) is open Element of bool the carrier of T
([#] T) /\ (V `) is Element of bool the carrier of T
(([#] T) /\ (V `)) ` is Element of bool the carrier of T
the carrier of T \ (([#] T) /\ (V `)) is set
Cl ((([#] T) /\ (V `)) `) is closed Element of bool the carrier of T
Int (Cl ((([#] T) /\ (V `)) `)) is open Element of bool the carrier of T
Cl ((V `) `) is closed Element of bool the carrier of T
Int (Cl ((V `) `)) is open Element of bool the carrier of T
E is Element of bool the carrier of T
a "/\" B is Element of the carrier of OL
(Int (C `)) /\ C is Element of bool the carrier of T
A ` is Element of bool the carrier of T
the carrier of T \ A is set
Int (A `) is open Element of bool the carrier of T
Int A is open Element of bool the carrier of T
(Int (A `)) /\ (Int A) is open Element of bool the carrier of T
(C `) /\ C is Element of bool the carrier of T
Int ((C `) /\ C) is open Element of bool the carrier of T
Int ({} T) is V1() V2() V3() empty open closed boundary nowhere_dense Element of bool the carrier of T
B "/\" a is Element of the carrier of OL
{} T is Element of bool the carrier of T
the carrier of OL is set
A is Element of the carrier of OL
B is Element of the carrier of OL
A "/\" B is Element of the carrier of OL
the L_meet of OL is V1() V4([: the carrier of OL, the carrier of OL:]) V5( the carrier of OL) Function-like V18([: the carrier of OL, the carrier of OL:], the carrier of OL) Element of bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:]
[: the carrier of OL, the carrier of OL:] is V1() set
[:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is V1() set
bool [:[: the carrier of OL, the carrier of OL:], the carrier of OL:] is non empty set
the L_meet of OL . (A,B) is Element of the carrier of OL
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
the L_meet of OL . [A,B] is set
B "/\" A is Element of the carrier of OL
the L_meet of OL . (B,A) is Element of the carrier of OL
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
the L_meet of OL . [B,A] is set
A "/\" B is Element of the carrier of OL
C is Element of (T)
A is Element of (T)
C /\ A is Element of bool the carrier of T
B "/\" A is Element of the carrier of OL
T is TopSpace-like TopStruct
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
T is TopSpace-like TopStruct
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) || (T) is V1() Function-like set
K5((T),[:(T),(T):]) is V1() V4([:(T),(T):]) V4([:(T),(T):]) V5((T)) set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
L is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
L . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
L . [A,B] is set
OL . (A,B) is Element of (T)
OL . [A,B] is set
(T) . (A,B) is set
(T) . [A,B] is set
[A,B] is Element of [:(T),(T):]
((T) || (T)) . [A,B] is set
T is TopSpace-like TopStruct
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) || (T) is V1() Function-like set
K5((T),[:(T),(T):]) is V1() V4([:(T),(T):]) V4([:(T),(T):]) V5((T)) set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
L is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
L . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
L . [A,B] is set
OL . (A,B) is Element of (T)
OL . [A,B] is set
(T) . (A,B) is set
(T) . [A,B] is set
[A,B] is Element of [:(T),(T):]
((T) || (T)) . [A,B] is set
T is TopSpace-like TopStruct
(T) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V86() complemented Boolean LattStr
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is closed_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
(T) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V86() complemented LattStr
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
the carrier of (T) is set
the carrier of (T) is set
the L_join of (T) is V1() V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) Function-like V18([: the carrier of (T), the carrier of (T):], the carrier of (T)) Element of bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):]
[: the carrier of (T), the carrier of (T):] is V1() set
[:[: the carrier of (T), the carrier of (T):], the carrier of (T):] is V1() set
bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):] is non empty set
the L_join of (T) is V1() V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) Function-like V18([: the carrier of (T), the carrier of (T):], the carrier of (T)) Element of bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):]
[: the carrier of (T), the carrier of (T):] is V1() set
[:[: the carrier of (T), the carrier of (T):], the carrier of (T):] is V1() set
bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):] is non empty set
the L_join of (T) || the carrier of (T) is V1() Function-like set
K5( the L_join of (T),[: the carrier of (T), the carrier of (T):]) is V1() V4([: the carrier of (T), the carrier of (T):]) V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) set
the L_meet of (T) is V1() V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) Function-like V18([: the carrier of (T), the carrier of (T):], the carrier of (T)) Element of bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):]
the L_meet of (T) is V1() V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) Function-like V18([: the carrier of (T), the carrier of (T):], the carrier of (T)) Element of bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):]
the L_meet of (T) || the carrier of (T) is V1() Function-like set
K5( the L_meet of (T),[: the carrier of (T), the carrier of (T):]) is V1() V4([: the carrier of (T), the carrier of (T):]) V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) set
T is TopSpace-like TopStruct
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) || (T) is V1() Function-like set
K5((T),[:(T),(T):]) is V1() V4([:(T),(T):]) V4([:(T),(T):]) V5((T)) set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
L is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
L . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
L . [A,B] is set
OL . (A,B) is Element of (T)
OL . [A,B] is set
(T) . (A,B) is set
(T) . [A,B] is set
[A,B] is Element of [:(T),(T):]
((T) || (T)) . [A,B] is set
T is TopSpace-like TopStruct
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) || (T) is V1() Function-like set
K5((T),[:(T),(T):]) is V1() V4([:(T),(T):]) V4([:(T),(T):]) V5((T)) set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
L is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
OL is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
A is Element of (T)
B is Element of (T)
L . (A,B) is Element of (T)
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
L . [A,B] is set
OL . (A,B) is Element of (T)
OL . [A,B] is set
(T) . (A,B) is set
(T) . [A,B] is set
[A,B] is Element of [:(T),(T):]
((T) || (T)) . [A,B] is set
T is TopSpace-like TopStruct
(T) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V86() complemented Boolean LattStr
(T) is non empty Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{ b1 where b1 is Element of bool the carrier of T : b1 is open_condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
(T) is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V86() complemented LattStr
(T) is non empty Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : b1 is condensed } is set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
[:(T),(T):] is V1() non empty set
[:[:(T),(T):],(T):] is V1() non empty set
bool [:[:(T),(T):],(T):] is non empty set
(T) is V1() V4([:(T),(T):]) V5((T)) Function-like V18([:(T),(T):],(T)) Element of bool [:[:(T),(T):],(T):]
LattStr(# (T),(T),(T) #) is non empty strict LattStr
the carrier of (T) is set
the carrier of (T) is set
the L_join of (T) is V1() V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) Function-like V18([: the carrier of (T), the carrier of (T):], the carrier of (T)) Element of bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):]
[: the carrier of (T), the carrier of (T):] is V1() set
[:[: the carrier of (T), the carrier of (T):], the carrier of (T):] is V1() set
bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):] is non empty set
the L_join of (T) is V1() V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) Function-like V18([: the carrier of (T), the carrier of (T):], the carrier of (T)) Element of bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):]
[: the carrier of (T), the carrier of (T):] is V1() set
[:[: the carrier of (T), the carrier of (T):], the carrier of (T):] is V1() set
bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):] is non empty set
the L_join of (T) || the carrier of (T) is V1() Function-like set
K5( the L_join of (T),[: the carrier of (T), the carrier of (T):]) is V1() V4([: the carrier of (T), the carrier of (T):]) V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) set
the L_meet of (T) is V1() V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) Function-like V18([: the carrier of (T), the carrier of (T):], the carrier of (T)) Element of bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):]
the L_meet of (T) is V1() V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) Function-like V18([: the carrier of (T), the carrier of (T):], the carrier of (T)) Element of bool [:[: the carrier of (T), the carrier of (T):], the carrier of (T):]
the L_meet of (T) || the carrier of (T) is V1() Function-like set
K5( the L_meet of (T),[: the carrier of (T), the carrier of (T):]) is V1() V4([: the carrier of (T), the carrier of (T):]) V4([: the carrier of (T), the carrier of (T):]) V5( the carrier of (T)) set