let X, Y be set ; :: thesis: subset-closed_closure_of (X \/ Y) = (subset-closed_closure_of X) \/ (subset-closed_closure_of Y)
set fxy = subset-closed_closure_of (X \/ Y);
set fx = subset-closed_closure_of X;
set fy = subset-closed_closure_of Y;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) c= subset-closed_closure_of (X \/ Y)

let x be object ; :: thesis: ( x in subset-closed_closure_of (X \/ Y) implies x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) )
reconsider xx = x as set by TARSKI:1;
assume x in subset-closed_closure_of (X \/ Y) ; :: thesis: x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y)
then consider y being set such that
A1: xx c= y and
A2: y in X \/ Y by Th2;
( y in X or y in Y ) by A2, XBOOLE_0:def 3;
then ( x in subset-closed_closure_of X or x in subset-closed_closure_of Y ) by A1, Th2;
hence x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) or x in subset-closed_closure_of (X \/ Y) )
reconsider xx = x as set by TARSKI:1;
assume A3: x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) ; :: thesis: x in subset-closed_closure_of (X \/ Y)

per cases ( x in subset-closed_closure_of X or x in subset-closed_closure_of Y ) by A3, XBOOLE_0:def 3;

suppose x in subset-closed_closure_of X ; :: thesis: x in subset-closed_closure_of (X \/ Y)

then consider y being set such that
A4: xx c= y and
A5: y in X by Th2;
y in X \/ Y by A5, XBOOLE_0:def 3;
hence x in subset-closed_closure_of (X \/ Y) by A4, Th2; :: thesis: verum

end;

suppose x in subset-closed_closure_of Y ; :: thesis: x in subset-closed_closure_of (X \/ Y)

then consider y being set such that
A6: xx c= y and
A7: y in Y by Th2;
y in X \/ Y by A7, XBOOLE_0:def 3;
hence x in subset-closed_closure_of (X \/ Y) by A6, Th2; :: thesis: verum

end;

end;