let T be non empty TopSpace; :: thesis: for FX, GX being Subset-Family of T holds clf (FX \/ GX) = (clf FX) \/ (clf GX)
let FX, GX be Subset-Family of T; :: thesis: clf (FX \/ GX) = (clf FX) \/ (clf GX)
for X being object holds
( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) )

proof

let X be object ; :: thesis: ( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) )

A1: now :: thesis: ( X in (clf FX) \/ (clf GX) implies X in clf (FX \/ GX) )

assume A2: X in (clf FX) \/ (clf GX) ; :: thesis: X in clf (FX \/ GX)

now :: thesis: X in clf (FX \/ GX)

per cases ( X in clf FX or X in clf GX ) by A2, XBOOLE_0:def 3;

suppose A3: X in clf FX ; :: thesis: X in clf (FX \/ GX)

then reconsider X9 = X as Subset of T ;
ex W being Subset of T st
( X9 = Cl W & W in FX \/ GX )

proof

consider Z being Subset of T such that
A4: ( X9 = Cl Z & Z in FX ) by A3, Def2;
take Z ; :: thesis: ( X9 = Cl Z & Z in FX \/ GX )
thus ( X9 = Cl Z & Z in FX \/ GX ) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

hence X in clf (FX \/ GX) by Def2; :: thesis: verum

end;

suppose A5: X in clf GX ; :: thesis: X in clf (FX \/ GX)

then reconsider X9 = X as Subset of T ;
ex W being Subset of T st
( X9 = Cl W & W in FX \/ GX )

proof

consider Z being Subset of T such that
A6: ( X9 = Cl Z & Z in GX ) by A5, Def2;
take Z ; :: thesis: ( X9 = Cl Z & Z in FX \/ GX )
thus ( X9 = Cl Z & Z in FX \/ GX ) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

hence X in clf (FX \/ GX) by Def2; :: thesis: verum

end;

end;

end;

hence X in clf (FX \/ GX) ; :: thesis: verum

end;

now :: thesis: ( X in clf (FX \/ GX) implies X in (clf FX) \/ (clf GX) )

assume A7: X in clf (FX \/ GX) ; :: thesis: X in (clf FX) \/ (clf GX)
then reconsider X9 = X as Subset of T ;
consider W being Subset of T such that
A8: X9 = Cl W and
A9: W in FX \/ GX by A7, Def2;

now :: thesis: X9 in (clf FX) \/ (clf GX)

per cases ( W in FX or W in GX ) by A9, XBOOLE_0:def 3;

suppose W in FX ; :: thesis: X9 in (clf FX) \/ (clf GX)

then X9 in clf FX by A8, Def2;
hence X9 in (clf FX) \/ (clf GX) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose W in GX ; :: thesis: X9 in (clf FX) \/ (clf GX)

then X9 in clf GX by A8, Def2;
hence X9 in (clf FX) \/ (clf GX) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence X in (clf FX) \/ (clf GX) ; :: thesis: verum

end;

hence ( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) ) by A1; :: thesis: verum

end;

hence clf (FX \/ GX) = (clf FX) \/ (clf GX) by TARSKI:2; :: thesis: verum