let A be Tolerance_Space; :: thesis: for X, Y being Subset of A holds UAp (X \/ Y) = (UAp X) \/ (UAp Y)
let X, Y be Subset of A; :: thesis: UAp (X \/ Y) = (UAp X) \/ (UAp Y)
thus UAp (X \/ Y) c= (UAp X) \/ (UAp Y) :: according to XBOOLE_0:def 10 :: thesis: (UAp X) \/ (UAp Y) c= UAp (X \/ Y)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp (X \/ Y) or x in (UAp X) \/ (UAp Y) )
assume A1: x in UAp (X \/ Y) ; :: thesis: x in (UAp X) \/ (UAp Y)
then Class ( the InternalRel of A,x) meets X \/ Y by Th10;
then ( Class ( the InternalRel of A,x) meets X or Class ( the InternalRel of A,x) meets Y ) by XBOOLE_1:70;
then ( x in UAp X or x in UAp Y ) by A1;
hence x in (UAp X) \/ (UAp Y) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UAp X) \/ (UAp Y) or x in UAp (X \/ Y) )
assume A2: x in (UAp X) \/ (UAp Y) ; :: thesis: x in UAp (X \/ Y)
then ( x in UAp X or x in UAp Y ) by XBOOLE_0:def 3;
then ( Class ( the InternalRel of A,x) meets X or Class ( the InternalRel of A,x) meets Y ) by Th10;
then Class ( the InternalRel of A,x) meets X \/ Y by XBOOLE_1:70;
hence x in UAp (X \/ Y) by A2; :: thesis: verum