let A, B be set ; :: thesis: for X being Subset of A
for R1, R2 being Subset of [:A,B:] st R1 c= R2 holds
R1 .:^ X c= R2 .:^ X
let X be Subset of A; :: thesis: for R1, R2 being Subset of [:A,B:] st R1 c= R2 holds
R1 .:^ X c= R2 .:^ X
let R1, R2 be Subset of [:A,B:]; :: thesis: ( R1 c= R2 implies R1 .:^ X c= R2 .:^ X )
assume A1: R1 c= R2 ; :: thesis: R1 .:^ X c= R2 .:^ X
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R1 .:^ X or y in R2 .:^ X )
assume A2: y in R1 .:^ X ; :: thesis: y in 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 (R2,x)

proof

let x be set ; :: thesis: ( x in X implies y in Im (R2,x) )
assume x in X ; :: thesis: y in Im (R2,x)
then y in Im (R1,x) by A2, Th25;
then [x,y] in R1 by Th9;
hence y in Im (R2,x) by A1, Th9; :: thesis: verum

end;

hence y in R2 .:^ X by Th25; :: thesis: verum