let T be non empty TopSpace; :: thesis: for X being Subset of (InclPoset the topology of T) holds sup X = union X
set L = InclPoset the topology of T;
let X be Subset of (InclPoset the topology of T); :: thesis: sup X = union X
reconsider X = X as Subset-Family of T by XBOOLE_1:1;
reconsider Un = union X as Element of (InclPoset the topology of T) by PRE_TOPC:def 1;

now

let b be Element of (InclPoset the topology of T); :: thesis: ( b in X implies b <= Un )
assume b in X ; :: thesis: b <= Un
then b c= Un by ZFMISC_1:92;
hence b <= Un by Th3; :: thesis: verum

end;

then A1: Un is_>=_than X by LATTICE3:def 9;

now

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

now

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

end;

then Un c= b by ZFMISC_1:94;
hence Un <= b by Th3; :: thesis: verum

end;

hence sup X = union X by A1, YELLOW_0:30; :: thesis: verum