let x be object ; :: thesis: for R1, R2 being Relation holds Im ((R1 \/ R2),x) = (Im (R1,x)) \/ (Im (R2,x))
let R1, R2 be Relation; :: thesis: Im ((R1 \/ R2),x) = (Im (R1,x)) \/ (Im (R2,x))
thus Im ((R1 \/ R2),x) c= (Im (R1,x)) \/ (Im (R2,x)) :: according to XBOOLE_0:def 10 :: thesis: (Im (R1,x)) \/ (Im (R2,x)) c= Im ((R1 \/ R2),x)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Im ((R1 \/ R2),x) or y in (Im (R1,x)) \/ (Im (R2,x)) )
assume y in Im ((R1 \/ R2),x) ; :: thesis: y in (Im (R1,x)) \/ (Im (R2,x))
then [x,y] in R1 \/ R2 by Th9;
then ( [x,y] in R1 or [x,y] in R2 ) by XBOOLE_0:def 3;
then ( y in Im (R1,x) or y in Im (R2,x) ) by Th9;
hence y in (Im (R1,x)) \/ (Im (R2,x)) by XBOOLE_0:def 3; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Im (R1,x)) \/ (Im (R2,x)) or y in Im ((R1 \/ R2),x) )
assume A1: y in (Im (R1,x)) \/ (Im (R2,x)) ; :: thesis: y in Im ((R1 \/ R2),x)
per cases ( y in Im (R1,x) or y in Im (R2,x) ) by A1, XBOOLE_0:def 3;
suppose y in Im (R1,x) ; :: thesis: y in Im ((R1 \/ R2),x)
then [x,y] in R1 by Th9;
then [x,y] in R1 \/ R2 by XBOOLE_0:def 3;
hence y in Im ((R1 \/ R2),x) by Th9; :: thesis: verum
end;
suppose y in Im (R2,x) ; :: thesis: y in Im ((R1 \/ R2),x)
then [x,y] in R2 by Th9;
then [x,y] in R1 \/ R2 by XBOOLE_0:def 3;
hence y in Im ((R1 \/ R2),x) by Th9; :: thesis: verum
end;
end;