:: TDLAT_1 semantic presentation

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
{ b₁ where b₁ is Element of bool the carrier of T : b₁ 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
{ b₁ where b₁ is Element of bool the carrier of T : b₁ 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
{ b₁ where b₁ is Element of bool the carrier of T : b₁ 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
{ b₁ where b₁ is Element of bool the carrier of T : b₁ 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
{ b₁ where b₁ is Element of bool the carrier of T : b₁ 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