let A, B be set ; :: thesis: for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X
let X be Subset of A; :: thesis: for R1, R2 being Subset of [:A,B:] holds (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X
let R1, R2 be Subset of [:A,B:]; :: thesis: (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (R1 .:^ X) \/ (R2 .:^ X) or y in (R1 \/ R2) .:^ X )
assume A1: y in (R1 .:^ X) \/ (R2 .:^ X) ; :: thesis: y in (R1 \/ R2) .:^ X

per cases ( y in R1 .:^ X or y in R2 .:^ X ) by A1, XBOOLE_0:def 3;

suppose A2: y in R1 .:^ X ; :: thesis: y in (R1 \/ R2) .:^ X

then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A2;
for x being set st x in X holds
y in Im ((R1 \/ R2),x)

proof

let x be set ; :: thesis: ( x in X implies y in Im ((R1 \/ R2),x) )
assume x in X ; :: thesis: y in Im ((R1 \/ R2),x)
then y in Im (R1,x) by A2, Th25;
then y in (Im (R1,x)) \/ (Im (R2,x)) by XBOOLE_0:def 3;
hence y in Im ((R1 \/ R2),x) by Th10; :: thesis: verum

end;

hence y in (R1 \/ R2) .:^ X by Th25; :: thesis: verum

end;

suppose A3: y in R2 .:^ X ; :: thesis: y in (R1 \/ R2) .:^ X

then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A3;
for x being set st x in X holds
y in Im ((R1 \/ R2),x)

proof

let x be set ; :: thesis: ( x in X implies y in Im ((R1 \/ R2),x) )
assume x in X ; :: thesis: y in Im ((R1 \/ R2),x)
then y in Im (R2,x) by A3, Th25;
then y in (Im (R1,x)) \/ (Im (R2,x)) by XBOOLE_0:def 3;
hence y in Im ((R1 \/ R2),x) by Th10; :: thesis: verum

end;

hence y in (R1 \/ R2) .:^ X by Th25; :: thesis: verum

end;

end;