let X, Y be set ; :: thesis: LeavesSet (X \/ Y) = (LeavesSet X) \/ (LeavesSet Y)
for x being object holds
( x in LeavesSet (X \/ Y) iff x in (LeavesSet X) \/ (LeavesSet Y) )

proof

let x be object ; :: thesis: ( x in LeavesSet (X \/ Y) iff x in (LeavesSet X) \/ (LeavesSet Y) )

hereby :: thesis: ( x in (LeavesSet X) \/ (LeavesSet Y) implies x in LeavesSet (X \/ Y) )

assume x in LeavesSet (X \/ Y) ; :: thesis: x in (LeavesSet X) \/ (LeavesSet Y)
then consider p being Element of BinFinTrees IndexedREAL such that
A1: ( x = Leaves p & p in X \/ Y ) ;
( p in X or p in Y ) by A1, XBOOLE_0:def 3;
then ( x in LeavesSet X or x in LeavesSet Y ) by A1;
hence x in (LeavesSet X) \/ (LeavesSet Y) by XBOOLE_0:def 3; :: thesis: verum

end;

assume A2: x in (LeavesSet X) \/ (LeavesSet Y) ; :: thesis: x in LeavesSet (X \/ Y)

per cases ( x in LeavesSet X or x in LeavesSet Y ) by A2, XBOOLE_0:def 3;

suppose x in LeavesSet X ; :: thesis: x in LeavesSet (X \/ Y)

then consider p being Element of BinFinTrees IndexedREAL such that
A3: ( x = Leaves p & p in X ) ;
p in X \/ Y by TARSKI:def 3, XBOOLE_1:7, A3;
hence x in LeavesSet (X \/ Y) by A3; :: thesis: verum

end;

suppose x in LeavesSet Y ; :: thesis: x in LeavesSet (X \/ Y)

then consider p being Element of BinFinTrees IndexedREAL such that
A4: ( x = Leaves p & p in Y ) ;
p in X \/ Y by TARSKI:def 3, XBOOLE_1:7, A4;
hence x in LeavesSet (X \/ Y) by A4; :: thesis: verum

end;

end;

end;

hence LeavesSet (X \/ Y) = (LeavesSet X) \/ (LeavesSet Y) by TARSKI:2; :: thesis: verum