let T be non empty TopSpace; :: thesis: InclPoset the topology of T is complete
set A = the topology of T;
reconsider IA = InclPoset the topology of T as lower-bounded Poset by Lm2;
for X being Subset of IA holds ex_sup_of X, InclPoset the topology of T

proof

let X be Subset of IA; :: thesis: ex_sup_of X, InclPoset the topology of T
set N = union X;
reconsider X9 = X as Subset-Family of T by XBOOLE_1:1;
X9 c= the topology of T ;
then reconsider N = union X as Element of (InclPoset the topology of T) by PRE_TOPC:def 1;
A1: for b being Element of (InclPoset the topology of T) st X is_<=_than b holds
N <= b

proof

let b be Element of (InclPoset the topology of T); :: thesis: ( X is_<=_than b implies N <= b )
assume A2: X is_<=_than b ; :: thesis: N <= b

now

let Z1 be set ; :: thesis: ( Z1 in X implies Z1 c= b )
assume A3: Z1 in X ; :: thesis: Z1 c= b
then reconsider Z19 = Z1 as Element of (InclPoset the topology of T) ;
Z19 <= b by A2, A3, LATTICE3:def 9;
hence Z1 c= b by Th3; :: thesis: verum

end;

then union X c= b by ZFMISC_1:76;
hence N <= b by Th3; :: thesis: verum

end;

X is_<=_than N

proof

let b be Element of (InclPoset the topology of T); :: according to LATTICE3:def 9 :: thesis: ( not b in X or b <= N )
assume b in X ; :: thesis: b <= N
then b c= N by ZFMISC_1:74;
hence b <= N by Th3; :: thesis: verum

end;

hence ex_sup_of X, InclPoset the topology of T by A1, YELLOW_0:15; :: thesis: verum

end;

hence InclPoset the topology of T is complete by YELLOW_0:53; :: thesis: verum