let T be non empty TopSpace; :: thesis: for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
let X be Subset of (Domains_Lattice T); :: thesis: ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
X c= the carrier of (Domains_Lattice T) ;
then A1: X c= Domains_of T by Th85;
then reconsider F = X as Subset-Family of T by TOPS_2:2;
set A = (union F) \/ (Int (Cl (union F)));
A2: F is domains-family by A1, Th64;
then (union F) \/ (Int (Cl (union F))) is condensed by Th67;
then (union F) \/ (Int (Cl (union F))) in { C where C is Subset of T : C is condensed } ;
then A3: (union F) \/ (Int (Cl (union F))) in Domains_of T by TDLAT_1:def 1;
then reconsider a = (union F) \/ (Int (Cl (union F))) as Element of (Domains_Lattice T) by Th85;
A4: for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b

proof

let b be Element of (Domains_Lattice T); :: thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Domains_of T by Th85;
assume A5: X is_less_than b ; :: thesis: a [= b
A6: for C being Subset of T st C in F holds
C c= B

proof

let C be Subset of T; :: thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of T ;
assume A7: C in F ; :: thesis: C c= B
then C1 is condensed by A2;
then C in { P where P is Subset of T : P is condensed } ;
then A8: C in Domains_of T by TDLAT_1:def 1;
then reconsider c = C as Element of (Domains_Lattice T) by Th85;
c [= b by A5, A7;
hence C c= B by A8, Th88; :: thesis: verum

end;

B in Domains_of T ;
then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def 1;
then ex C being Subset of T st
( C = B & C is condensed ) ;
then (union F) \/ (Int (Cl (union F))) c= B by A6, Th68;
hence a [= b by A3, Th88; :: thesis: verum

end;

take a ; :: thesis: ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )
X is_less_than a

proof

let b be Element of (Domains_Lattice T); :: according to LATTICE3:def 17 :: thesis: ( not b in X or b [= a )
reconsider B = b as Element of Domains_of T by Th85;
assume b in X ; :: thesis: b [= a
then B c= (union F) \/ (Int (Cl (union F))) by Th68;
hence b [= a by A3, Th88; :: thesis: verum

end;

hence ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) ) by A4; :: thesis: verum