let y be object ; :: thesis:
let A, B be set ; :: thesis:
let X be Subset of A; :: thesis:
let R be Subset of [:A,B:]; :: thesis:
assume A1: y in R .:^ X ; :: thesis:

per cases ) .: {_{X}_} = {} or (.: R) .: {_{X}_} <> {} ) ;

suppose (.: R) .: {_{X}_} = {} ; :: thesis:

hence for x being set st x in X holds
y in Im (R,x) by Th23; :: thesis:

end;

suppose (.: R) .: {_{X}_} <> {} ; :: thesis:

then A2: y in meet ((.: R) .: {_{X}_}) by A1, SETFAM_1:def 9;
for x being set st x in X holds
y in R .: {x}

proof

let x be set ; :: thesis:
assume A3: x in X ; :: thesis:
then A4: {x} in {_{X}_} by Th1;
A5: {x} c= A

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in {x} ; :: thesis:
then a = x by TARSKI:def 1;
hence a in A by A3; :: thesis:

end;

then A6: (.: R) . {x} = R .: {x} by Def1;
dom (.: R) = bool A by Def1;
then [{x},(R .: {x})] in .: R by A5, A6, FUNCT_1:1;
then R .: {x} in (.: R) .: {_{X}_} by A4, RELAT_1:def 13;
hence y in R .: {x} by A2, SETFAM_1:def 1; :: thesis:

end;

hence for x being set st x in X holds
y in Im (R,x) ; :: thesis:

end;

end;