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 X is_<=_than b ; :: thesis: N <= b
then for Z1 being set st Z1 in X holds
Z1 c= b by Th3;
then union X c= b by ZFMISC_1:76;
hence N <= b by Th3; :: thesis: verum

end;

X is_<=_than N by ZFMISC_1:74, Th3;
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