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;

A1: now :: thesis: for b being Element of (InclPoset the topology of T) st b is_>=_than X holds
Un <= b

let b be Element of (InclPoset the topology of T); :: thesis: ( b is_>=_than X implies Un <= b )
assume b is_>=_than X ; :: thesis: Un <= b
then for Z being set st Z in X holds
Z c= b by Th3;
then Un c= b by ZFMISC_1:76;
hence Un <= b by Th3; :: thesis: verum

end;

for b being Element of (InclPoset the topology of T) st b in X holds
b <= Un by Th3, ZFMISC_1:74;
then Un is_>=_than X ;
hence sup X = union X by A1, YELLOW_0:30; :: thesis: verum