let X, Y be set ; :: thesis: for R being Relation holds R .: (X \/ Y) = (R .: X) \/ (R .: Y)
let R be Relation; :: thesis: R .: (X \/ Y) = (R .: X) \/ (R .: Y)
thus R .: (X \/ Y) c= (R .: X) \/ (R .: Y) :: according to XBOOLE_0:def 10 :: thesis: (R .: X) \/ (R .: Y) c= R .: (X \/ Y)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: (X \/ Y) or y in (R .: X) \/ (R .: Y) )
assume y in R .: (X \/ Y) ; :: thesis: y in (R .: X) \/ (R .: Y)
then consider x being object such that
A1: [x,y] in R and
A2: x in X \/ Y by Def11;
( x in X or x in Y ) by A2, XBOOLE_0:def 3;
then ( y in R .: X or y in R .: Y ) by A1, Def11;
hence y in (R .: X) \/ (R .: Y) by XBOOLE_0:def 3; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (R .: X) \/ (R .: Y) or y in R .: (X \/ Y) )
assume A3: y in (R .: X) \/ (R .: Y) ; :: thesis: y in R .: (X \/ Y)
per cases ( y in R .: Y or y in R .: X ) by A3, XBOOLE_0:def 3;
suppose y in R .: Y ; :: thesis: y in R .: (X \/ Y)
then consider x being object such that
A4: [x,y] in R and
A5: x in Y by Def11;
x in X \/ Y by A5, XBOOLE_0:def 3;
hence y in R .: (X \/ Y) by A4, Def11; :: thesis: verum
end;
suppose y in R .: X ; :: thesis: y in R .: (X \/ Y)
then consider x being object such that
A6: [x,y] in R and
A7: x in X by Def11;
x in X \/ Y by A7, XBOOLE_0:def 3;
hence y in R .: (X \/ Y) by A6, Def11; :: thesis: verum
end;
end;