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 set holds
( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) )

proof

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

A1: now

assume A2: X in clf (FX \/ GX) ; :: thesis: X in (clf FX) \/ (clf GX)
then reconsider X' = X as Subset of T ;
consider W being Subset of T such that
A3: X' = Cl W and
A4: W in FX \/ GX by A2, Def3;

now

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

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

then X' in clf FX by A3, Def3;
hence X' in (clf FX) \/ (clf GX) by XBOOLE_0:def 3; :: thesis: verum

end;

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

then X' in clf GX by A3, Def3;
hence X' 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;

now

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

now

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

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

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

proof

consider Z being Subset of T such that
A7: X' = Cl Z and
A8: Z in FX by A6, Def3;
take Z ; :: thesis: ( X' = Cl Z & Z in FX \/ GX )
thus ( X' = Cl Z & Z in FX \/ GX ) by A7, A8, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

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

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

proof

consider Z being Subset of T such that
A10: X' = Cl Z and
A11: Z in GX by A9, Def3;
take Z ; :: thesis: ( X' = Cl Z & Z in FX \/ GX )
thus ( X' = Cl Z & Z in FX \/ GX ) by A10, A11, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

end;

end;

hence X in clf (FX \/ 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