let R be non empty RelStr ; :: thesis: for X, Y being Subset of R holds UAp (X \/ Y) = (UAp X) \/ (UAp Y)
let X, Y be Subset of R; :: 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 y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in UAp (X \/ Y) or y in (UAp X) \/ (UAp Y) )
assume y in UAp (X \/ Y) ; :: thesis: y in (UAp X) \/ (UAp Y)
then consider z being Element of R such that
A1: ( z = y & Class ( the InternalRel of R,z) meets X \/ Y ) ;
( Class ( the InternalRel of R,z) meets X or Class ( the InternalRel of R,z) meets Y ) by A1, XBOOLE_1:70;
then ( z in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } or z in { x where x is Element of R : Class ( the InternalRel of R,x) meets Y } ) ;
hence y in (UAp X) \/ (UAp Y) by A1, XBOOLE_0:def 3; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (UAp X) \/ (UAp Y) or y in UAp (X \/ Y) )
assume y in (UAp X) \/ (UAp Y) ; :: thesis: y in UAp (X \/ Y)
per cases then ( y in UAp X or y in UAp Y ) by XBOOLE_0:def 3;
suppose y in UAp X ; :: thesis: y in UAp (X \/ Y)
then consider z being Element of R such that
A2: ( z = y & Class ( the InternalRel of R,z) meets X ) ;
Class ( the InternalRel of R,z) meets X \/ Y by A2, XBOOLE_1:70;
hence y in UAp (X \/ Y) by A2; :: thesis: verum
end;
suppose y in UAp Y ; :: thesis: y in UAp (X \/ Y)
then consider z being Element of R such that
A3: ( z = y & Class ( the InternalRel of R,z) meets Y ) ;
Class ( the InternalRel of R,z) meets X \/ Y by A3, XBOOLE_1:70;
hence y in UAp (X \/ Y) by A3; :: thesis: verum
end;
end;