let GX be TopSpace; :: thesis: for W being Subset-Family of GX st W is open holds
union W is open
let W be Subset-Family of GX; :: thesis: ( W is open implies union W is open )
assume A1: W is open ; :: thesis: union W is open
W c= the topology of GX

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in the topology of GX )
assume A2: x in W ; :: thesis: x in the topology of GX
then reconsider X = x as Subset of GX ;
X is open by A1, A2;
hence x in the topology of GX ; :: thesis: verum

end;

then union W in the topology of GX by PRE_TOPC:def 1;
hence union W is open ; :: thesis: verum