let A be Tolerance_Space; :: thesis: for X, Y being Subset of A holds (LAp X) \/ (LAp Y) c= LAp (X \/ Y)
let X, Y be Subset of A; :: thesis: (LAp X) \/ (LAp Y) c= LAp (X \/ Y)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LAp X) \/ (LAp Y) or x in LAp (X \/ Y) )
assume A1: x in (LAp X) \/ (LAp Y) ; :: thesis: x in LAp (X \/ Y)

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

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

then Class ( the InternalRel of A,x) c= X \/ Y by Th8, XBOOLE_1:10;
hence x in LAp (X \/ Y) by A1; :: thesis: verum

end;

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

then Class ( the InternalRel of A,x) c= X \/ Y by Th8, XBOOLE_1:10;
hence x in LAp (X \/ Y) by A1; :: thesis: verum

end;

end;