let GX be TopSpace; :: thesis: for A, B being Subset of GX holds Cl (A \/ B) = (Cl A) \/ (Cl B)
let A, B be Subset of GX; :: thesis: Cl (A \/ B) = (Cl A) \/ (Cl B)

now :: thesis: for x being object st x in Cl (A \/ B) holds
x in (Cl A) \/ (Cl B)

let x be object ; :: thesis: ( x in Cl (A \/ B) implies x in (Cl A) \/ (Cl B) )
assume A1: x in Cl (A \/ B) ; :: thesis: x in (Cl A) \/ (Cl B)
assume A2: not x in (Cl A) \/ (Cl B) ; :: thesis: contradiction
then not x in Cl A by XBOOLE_0:def 3;
then consider G1 being Subset of GX such that
A3: G1 is open and
A4: x in G1 and
A5: A misses G1 by A1, Def7;
A6: A /\ G1 = {} by A5, XBOOLE_0:def 7;
not x in Cl B by A2, XBOOLE_0:def 3;
then consider G2 being Subset of GX such that
A7: G2 is open and
A8: x in G2 and
A9: B misses G2 by A1, Def7;
A10: G2 in the topology of GX by A7;
A11: B /\ G2 = {} by A9, XBOOLE_0:def 7;
(A \/ B) /\ (G1 /\ G2) = (A /\ (G1 /\ G2)) \/ (B /\ (G2 /\ G1)) by XBOOLE_1:23
.= ((A /\ G1) /\ G2) \/ (B /\ (G2 /\ G1)) by XBOOLE_1:16
.= {} \/ ({} /\ G1) by A6, A11, XBOOLE_1:16
.= {} GX ;
then A12: A \/ B misses G1 /\ G2 by XBOOLE_0:def 7;
G1 in the topology of GX by A3;
then G1 /\ G2 in the topology of GX by A10, Def1;
then A13: G1 /\ G2 is open ;
x in G1 /\ G2 by A4, A8, XBOOLE_0:def 4;
hence contradiction by A1, A13, A12, Def7; :: thesis: verum

end;

then A14: Cl (A \/ B) c= (Cl A) \/ (Cl B) ;
( Cl A c= Cl (A \/ B) & Cl B c= Cl (A \/ B) ) by Th19, XBOOLE_1:7;
then (Cl A) \/ (Cl B) c= Cl (A \/ B) by XBOOLE_1:8;
hence Cl (A \/ B) = (Cl A) \/ (Cl B) by A14, XBOOLE_0:def 10; :: thesis: verum