let y be object ; :: thesis: for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)
let A, B be set ; :: thesis: for X being Subset of A
for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)
let X be Subset of A; :: thesis: for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)
let R be Subset of [:A,B:]; :: thesis: ( y in R .:^ X implies for x being set st x in X holds
y in Im (R,x) )
assume A1: y in R .:^ X ; :: thesis: for x being set st x in X holds
y in Im (R,x)

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

suppose (.: R) .: {_{X}_} = {} ; :: thesis: for x being set st x in X holds
y in Im (R,x)

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

end;

suppose (.: R) .: {_{X}_} <> {} ; :: thesis: for x being set st x in X holds
y in Im (R,x)

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: ( x in X implies y in R .: {x} )
assume A3: x in X ; :: thesis: y in R .: {x}
then A4: {x} in {_{X}_} by Th1;
A5: {x} c= A

proof

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

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: verum

end;

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

end;

end;