:: YELLOW13 semantic presentation

registration
let c1 be finite 1-sorted ;
cluster the carrier of a1 -> finite ;
coherence
the carrier of c1 is finite by GROUP_1:def 14;
end;

registration
let c1 be trivial 1-sorted ;
cluster the carrier of a1 -> trivial ;
coherence
the carrier of c1 is trivial by REALSET2:def 5;
end;

registration
cluster trivial -> finite set ;
coherence
for b1 being set st b1 is trivial holds
b1 is finite
proof end;
end;

registration
cluster trivial -> finite 1-sorted ;
coherence
for b1 being 1-sorted st b1 is trivial holds
b1 is finite
proof end;
end;

registration
cluster non trivial -> non empty 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is trivial holds
not b1 is empty
proof end;
end;

registration
cluster strict non empty finite trivial 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
cluster non empty strict finite trivial RelStr ;
existence
ex b1 being RelStr st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
cluster non empty strict finite trivial TopRelStr ;
existence
ex b1 being TopRelStr st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

theorem Th1: :: YELLOW13:1
for b1 being non empty being_T1 TopSpace
for b2 being finite Subset of b1 holds b2 is closed
proof end;

registration
let c1 be non empty being_T1 TopSpace;
cluster finite -> closed Element of bool the carrier of a1;
coherence
for b1 being Subset of c1 st b1 is finite holds
b1 is closed by Th1;
end;

registration
let c1 be compact TopStruct ;
cluster [#] a1 -> compact ;
coherence
[#] c1 is compact by COMPTS_1:10;
end;

registration
cluster non empty strict finite trivial TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

registration
cluster non empty being_T1 finite -> non empty discrete TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is finite & b1 is being_T1 holds
b1 is discrete
proof end;
end;

registration
cluster finite -> compact TopStruct ;
coherence
for b1 being TopSpace st b1 is finite holds
b1 is compact
proof end;
end;

theorem Th2: :: YELLOW13:2
for b1 being non empty discrete TopSpace holds b1 is_T4
proof end;

theorem Th3: :: YELLOW13:3
for b1 being non empty discrete TopSpace holds b1 is_T3
proof end;

theorem Th4: :: YELLOW13:4
for b1 being non empty discrete TopSpace holds b1 is_T2
proof end;

theorem Th5: :: YELLOW13:5
for b1 being non empty discrete TopSpace holds b1 is_T1
proof end;

registration
cluster non empty discrete -> being_T1 being_T2 being_T3 being_T4 TopStruct ;
coherence
for b1 being TopSpace st b1 is discrete & not b1 is empty holds
( b1 is being_T4 & b1 is being_T3 & b1 is being_T2 & b1 is being_T1 ) by Th2, Th3, Th4, Th5;
end;

registration
cluster non empty being_T1 being_T4 -> non empty being_T3 TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is being_T4 & b1 is being_T1 holds
b1 is being_T3
proof end;
end;

registration
cluster being_T1 being_T3 -> being_T2 TopStruct ;
coherence
for b1 being TopSpace st b1 is being_T3 & b1 is being_T1 holds
b1 is being_T2
proof end;
end;

registration
cluster being_T2 -> being_T1 TopStruct ;
coherence
for b1 being TopSpace st b1 is being_T2 holds
b1 is being_T1
proof end;
end;

registration
cluster being_T1 -> T_0 TopStruct ;
coherence
for b1 being TopSpace st b1 is being_T1 holds
b1 is T_0
proof end;
end;

theorem Th6: :: YELLOW13:6
for b1 being reflexive RelStr
for b2 being reflexive transitive RelStr
for b3 being Function of b1,b2
for b4 being Subset of b1 holds downarrow (b3 .: b4) c= downarrow (b3 .: (downarrow b4))
proof end;

theorem Th7: :: YELLOW13:7
for b1 being reflexive RelStr
for b2 being reflexive transitive RelStr
for b3 being Function of b1,b2
for b4 being Subset of b1 st b3 is monotone holds
downarrow (b3 .: b4) = downarrow (b3 .: (downarrow b4))
proof end;

theorem Th8: :: YELLOW13:8
for b1 being non empty Poset holds IdsMap b1 is one-to-one
proof end;

registration
let c1 be non empty Poset;
cluster IdsMap a1 -> V6 ;
coherence
IdsMap c1 is one-to-one by Th8;
end;

theorem Th9: :: YELLOW13:9
for b1 being finite LATTICE holds SupMap b1 is one-to-one
proof end;

registration
let c1 be finite LATTICE;
cluster SupMap a1 -> V6 ;
coherence
SupMap c1 is one-to-one by Th9;
end;

theorem Th10: :: YELLOW13:10
for b1 being finite LATTICE holds b1, InclPoset (Ids b1) are_isomorphic
proof end;

theorem Th11: :: YELLOW13:11
for b1 being non empty complete Poset
for b2 being Element of b1
for b3 being non empty Subset of b1 holds b2 "/\" preserves_inf_of b3
proof end;

theorem Th12: :: YELLOW13:12
for b1 being non empty complete Poset
for b2 being Element of b1 holds b2 "/\" is meet-preserving
proof end;

registration
let c1 be non empty complete Poset;
let c2 be Element of c1;
cluster a2 "/\" -> meet-preserving ;
coherence
c2 "/\" is meet-preserving by Th12;
end;

theorem Th13: :: YELLOW13:13
for b1 being non empty anti-discrete TopStruct
for b2 being Point of b1 holds {the carrier of b1} is Basis of b2
proof end;

theorem Th14: :: YELLOW13:14
for b1 being non empty anti-discrete TopStruct
for b2 being Point of b1
for b3 being Basis of b2 holds b3 = {the carrier of b1}
proof end;

theorem Th15: :: YELLOW13:15
for b1 being non empty TopSpace
for b2 being Basis of b1
for b3 being Point of b1 holds { b4 where B is Subset of b1 : ( b4 in b2 & b3 in b4 ) } is Basis of b3
proof end;

Lemma11: for b1 being non empty TopStruct
for b2 being Subset of b1
for b3 being Point of b1 st b3 in Cl b2 holds
for b4 being Basis of b3
for b5 being Subset of b1 st b5 in b4 holds
b2 meets b5
proof end;

Lemma12: for b1 being non empty TopStruct
for b2 being Subset of b1
for b3 being Point of b1 st ( for b4 being Basis of b3
for b5 being Subset of b1 st b5 in b4 holds
b2 meets b5 ) holds
ex b4 being Basis of b3 st
for b5 being Subset of b1 st b5 in b4 holds
b2 meets b5
proof end;

Lemma13: for b1 being non empty TopStruct
for b2 being Subset of b1
for b3 being Point of b1 st ex b4 being Basis of b3 st
for b5 being Subset of b1 st b5 in b4 holds
b2 meets b5 holds
b3 in Cl b2
proof end;

theorem Th16: :: YELLOW13:16
for b1 being non empty TopStruct
for b2 being Subset of b1
for b3 being Point of b1 holds
( b3 in Cl b2 iff for b4 being Basis of b3
for b5 being Subset of b1 st b5 in b4 holds
b2 meets b5 )
proof end;

theorem Th17: :: YELLOW13:17
for b1 being non empty TopStruct
for b2 being Subset of b1
for b3 being Point of b1 holds
( b3 in Cl b2 iff ex b4 being Basis of b3 st
for b5 being Subset of b1 st b5 in b4 holds
b2 meets b5 )
proof end;

definition
let c1 be TopStruct ;
let c2 be Point of c1;
mode basis of c2 -> Subset-Family of a1 means :Def1: :: YELLOW13:def 1
for b1 being Subset of a1 st a2 in Int b1 holds
ex b2 being Subset of a1 st
( b2 in a3 & a2 in Int b2 & b2 c= b1 );
existence
ex b1 being Subset-Family of c1 st
for b2 being Subset of c1 st c2 in Int b2 holds
ex b3 being Subset of c1 st
( b3 in b1 & c2 in Int b3 & b3 c= b2 )
proof end;
end;

:: deftheorem Def1 defines basis YELLOW13:def 1 :
for b1 being TopStruct
for b2 being Point of b1
for b3 being Subset-Family of b1 holds
( b3 is basis of b2 iff for b4 being Subset of b1 st b2 in Int b4 holds
ex b5 being Subset of b1 st
( b5 in b3 & b2 in Int b5 & b5 c= b4 ) );

definition
let c1 be non empty TopSpace;
let c2 be Point of c1;
redefine mode basis of c2 -> Subset-Family of a1 means :: YELLOW13:def 2
for b1 being a_neighborhood of a2 ex b2 being a_neighborhood of a2 st
( b2 in a3 & b2 c= b1 );
compatibility
for b1 being Subset-Family of c1 holds
( b1 is basis of c2 iff for b2 being a_neighborhood of c2 ex b3 being a_neighborhood of c2 st
( b3 in b1 & b3 c= b2 ) )
proof end;
end;

:: deftheorem Def2 defines basis YELLOW13:def 2 :
for b1 being non empty TopSpace
for b2 being Point of b1
for b3 being Subset-Family of b1 holds
( b3 is basis of b2 iff for b4 being a_neighborhood of b2 ex b5 being a_neighborhood of b2 st
( b5 in b3 & b5 c= b4 ) );

theorem Th18: :: YELLOW13:18
for b1 being TopStruct
for b2 being Point of b1 holds bool the carrier of b1 is basis of b2
proof end;

theorem Th19: :: YELLOW13:19
for b1 being non empty TopSpace
for b2 being Point of b1
for b3 being basis of b2 holds not b3 is empty
proof end;

registration
let c1 be non empty TopSpace;
let c2 be Point of c1;
cluster -> non empty basis of a2;
coherence
for b1 being basis of c2 holds not b1 is empty by Th19;
end;

registration
let c1 be TopStruct ;
let c2 be Point of c1;
cluster non empty basis of a2;
existence
not for b1 being basis of c2 holds b1 is empty
proof end;
end;

definition
let c1 be TopStruct ;
let c2 be Point of c1;
let c3 be basis of c2;
attr a3 is correct means :Def3: :: YELLOW13:def 3
for b1 being Subset of a1 holds
( b1 in a3 iff a2 in Int b1 );
end;

:: deftheorem Def3 defines correct YELLOW13:def 3 :
for b1 being TopStruct
for b2 being Point of b1
for b3 being basis of b2 holds
( b3 is correct iff for b4 being Subset of b1 holds
( b4 in b3 iff b2 in Int b4 ) );

E18: now
let c1 be TopStruct ;
let c2 be Point of c1;
let c3 be set ;
assume E19: c3 = { b1 where B is Subset of c1 : c2 in Int b1 } ;
c3 c= bool the carrier of c1
proof
let c4 be set ; :: according to TARSKI:def 3
assume c4 in c3 ;
then consider c5 being Subset of c1 such that
E20: c4 = c5 and
c2 in Int c5 by E19;
thus c4 in bool the carrier of c1 by E20;
end;
then reconsider c4 = c3 as Subset-Family of c1 ;
reconsider c5 = c4 as Subset-Family of c1 ;
for b1 being Subset of c1 st c2 in Int b1 holds
ex b2 being Subset of c1 st
( b2 in c5 & c2 in Int b2 & b2 c= b1 )
proof
let c6 be Subset of c1;
assume E20: c2 in Int c6 ;
take c7 = c6;
thus ( c7 in c5 & c2 in Int c7 & c7 c= c6 ) by E19, E20;
end;
hence c3 is basis of c2 by Def1;
end;

E19: now
let c1 be TopStruct ;
let c2 be Point of c1;
let c3 be basis of c2;
assume E20: c3 = { b1 where B is Subset of c1 : c2 in Int b1 } ;
thus c3 is correct
proof
let c4 be Subset of c1; :: according to YELLOW13:def 3
hereby
assume c4 in c3 ;
then consider c5 being Subset of c1 such that
E21: ( c4 = c5 & c2 in Int c5 ) by E20;
thus c2 in Int c4 by E21;
end;
thus ( c2 in Int c4 implies c4 in c3 ) by E20;
end;
end;

registration
let c1 be TopStruct ;
let c2 be Point of c1;
cluster correct basis of a2;
existence
ex b1 being basis of c2 st b1 is correct
proof end;
end;

theorem Th20: :: YELLOW13:20
for b1 being TopStruct
for b2 being Point of b1 holds { b3 where B is Subset of b1 : b2 in Int b3 } is correct basis of b2 by Lemma18, Lemma19;

registration
let c1 be non empty TopSpace;
let c2 be Point of c1;
cluster non empty correct basis of a2;
existence
ex b1 being basis of c2 st
( not b1 is empty & b1 is correct )
proof end;
end;

theorem Th21: :: YELLOW13:21
for b1 being non empty anti-discrete TopStruct
for b2 being Point of b1 holds {the carrier of b1} is correct basis of b2
proof end;

theorem Th22: :: YELLOW13:22
for b1 being non empty anti-discrete TopStruct
for b2 being Point of b1
for b3 being correct basis of b2 holds b3 = {the carrier of b1}
proof end;

theorem Th23: :: YELLOW13:23
for b1 being non empty TopSpace
for b2 being Point of b1
for b3 being Basis of b2 holds b3 is basis of b2
proof end;

definition
let c1 be TopStruct ;
mode basis of c1 -> Subset-Family of a1 means :Def4: :: YELLOW13:def 4
for b1 being Point of a1 holds a2 is basis of b1;
existence
ex b1 being Subset-Family of c1 st
for b2 being Point of c1 holds b1 is basis of b2
proof end;
end;

:: deftheorem Def4 defines basis YELLOW13:def 4 :
for b1 being TopStruct
for b2 being Subset-Family of b1 holds
( b2 is basis of b1 iff for b3 being Point of b1 holds b2 is basis of b3 );

theorem Th24: :: YELLOW13:24
for b1 being TopStruct holds bool the carrier of b1 is basis of b1
proof end;

theorem Th25: :: YELLOW13:25
for b1 being non empty TopSpace
for b2 being basis of b1 holds not b2 is empty
proof end;

registration
let c1 be non empty TopSpace;
cluster -> non empty basis of a1;
coherence
for b1 being basis of c1 holds not b1 is empty by Th25;
end;

registration
let c1 be TopStruct ;
cluster non empty basis of a1;
existence
not for b1 being basis of c1 holds b1 is empty
proof end;
end;

theorem Th26: :: YELLOW13:26
for b1 being non empty TopSpace
for b2 being basis of b1 holds the topology of b1 c= UniCl (Int b2)
proof end;

theorem Th27: :: YELLOW13:27
for b1 being TopSpace
for b2 being Basis of b1 holds b2 is basis of b1
proof end;

definition
let c1 be non empty TopSpace-like TopRelStr ;
attr a1 is topological_semilattice means :Def5: :: YELLOW13:def 5
for b1 being Function of [:a1,a1:],a1 st b1 = inf_op a1 holds
b1 is continuous;
end;

:: deftheorem Def5 defines topological_semilattice YELLOW13:def 5 :
for b1 being non empty TopSpace-like TopRelStr holds
( b1 is topological_semilattice iff for b2 being Function of [:b1,b1:],b1 st b2 = inf_op b1 holds
b2 is continuous );

registration
cluster non empty TopSpace-like reflexive trivial -> non empty TopSpace-like topological_semilattice TopRelStr ;
coherence
for b1 being non empty TopSpace-like TopRelStr st b1 is reflexive & b1 is trivial holds
b1 is topological_semilattice
proof end;
end;

registration
cluster non empty TopSpace-like T_0 being_T1 reflexive compact being_T2 being_T3 being_T4 finite trivial topological_semilattice TopRelStr ;
existence
ex b1 being TopRelStr st
( b1 is reflexive & b1 is trivial & not b1 is empty & b1 is TopSpace-like )
proof end;
end;

theorem Th28: :: YELLOW13:28
for b1 being non empty TopSpace-like topological_semilattice TopRelStr
for b2 being Element of b1 holds b2 "/\" is continuous
proof end;

registration
let c1 be non empty TopSpace-like topological_semilattice TopRelStr ;
let c2 be Element of c1;
cluster a2 "/\" -> continuous ;
coherence
c2 "/\" is continuous by Th28;
end;