let T be non empty TopSpace; :: thesis: Open_Domains_Lattice T is complete
thus for X being set ex a being Element of (Open_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) ) :: according to LATTICE3:def 18 :: thesis: verum
proof
let X be set ; :: thesis: ex a being Element of (Open_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
set Y = { c where c is Element of (Open_Domains_Lattice T) : c in X } ;
A1: for d being Element of (Open_Domains_Lattice T) st { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d holds
X is_less_than d
proof
let d be Element of (Open_Domains_Lattice T); :: thesis: ( { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d implies X is_less_than d )
assume A2: { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d ; :: thesis: X is_less_than d
thus for e being Element of (Open_Domains_Lattice T) st e in X holds
e [= d :: according to LATTICE3:def 17 :: thesis: verum
proof
let e be Element of (Open_Domains_Lattice T); :: thesis: ( e in X implies e [= d )
assume e in X ; :: thesis: e [= d
then e in { c where c is Element of (Open_Domains_Lattice T) : c in X } ;
hence e [= d by A2; :: thesis: verum
end;
end;
A3: for d being Element of (Open_Domains_Lattice T) st X is_less_than d holds
{ c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d
proof
let d be Element of (Open_Domains_Lattice T); :: thesis: ( X is_less_than d implies { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d )
assume A4: X is_less_than d ; :: thesis: { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d
thus for e being Element of (Open_Domains_Lattice T) st e in { c where c is Element of (Open_Domains_Lattice T) : c in X } holds
e [= d :: according to LATTICE3:def 17 :: thesis: verum
proof
let e be Element of (Open_Domains_Lattice T); :: thesis: ( e in { c where c is Element of (Open_Domains_Lattice T) : c in X } implies e [= d )
assume e in { c where c is Element of (Open_Domains_Lattice T) : c in X } ; :: thesis: e [= d
then ex e0 being Element of (Open_Domains_Lattice T) st
( e0 = e & e0 in X ) ;
hence e [= d by A4; :: thesis: verum
end;
end;
now :: thesis: for x being object st x in { c where c is Element of (Open_Domains_Lattice T) : c in X } holds
x in the carrier of (Open_Domains_Lattice T)
let x be object ; :: thesis: ( x in { c where c is Element of (Open_Domains_Lattice T) : c in X } implies x in the carrier of (Open_Domains_Lattice T) )
assume x in { c where c is Element of (Open_Domains_Lattice T) : c in X } ; :: thesis: x in the carrier of (Open_Domains_Lattice T)
then ex y being Element of (Open_Domains_Lattice T) st
( y = x & y in X ) ;
hence x in the carrier of (Open_Domains_Lattice T) ; :: thesis: verum
end;
then reconsider Y = { c where c is Element of (Open_Domains_Lattice T) : c in X } as Subset of (Open_Domains_Lattice T) by TARSKI:def 3;
consider a being Element of (Open_Domains_Lattice T) such that
A5: Y is_less_than a and
A6: for b being Element of (Open_Domains_Lattice T) st Y is_less_than b holds
a [= b by Th106;
take a ; :: thesis: ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )
for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b by A3, A6;
hence ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) ) by A1, A5; :: thesis: verum
end;