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

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

{} 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

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

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

(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