let B be non empty set ; :: thesis: for A being set
for X being Subset of A
for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im R,x )
let A be set ; :: thesis: for X being Subset of A
for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im R,x )
let X be Subset of A; :: thesis: for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im R,x )
let y be Element of B; :: thesis: for R being Subset of [:A,B:] holds
( y in R .:^ X iff 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 iff for x being set st x in X holds
y in Im R,x )
thus ( y in R .:^ X implies for x being set st x in X holds
y in Im R,x ) by Th24; :: thesis: ( ( for x being set st x in X holds
y in Im R,x ) implies y in R .:^ X )
assume A1: for x being set st x in X holds
y in Im R,x ; :: thesis: y in R .:^ X

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

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

then Intersect ((.: R) .: {_{X}_}) = B by SETFAM_1:def 10;
hence y in R .:^ X ; :: thesis: verum

end;

suppose A2: (.: R) .: {_{X}_} <> {} ; :: thesis: y in R .:^ X

then A3: Intersect ((.: R) .: {_{X}_}) = meet ((.: R) .: {_{X}_}) by SETFAM_1:def 10;
for Y being set st Y in (.: R) .: {_{X}_} holds
y in Y

proof

let Y be set ; :: thesis: ( Y in (.: R) .: {_{X}_} implies y in Y )
assume Y in (.: R) .: {_{X}_} ; :: thesis: y in Y
then consider z being set such that
A4: ( [z,Y] in .: R & z in {_{X}_} ) by RELAT_1:def 13;
consider x being set such that
A5: ( z = {x} & x in X ) by A4, Th1;
( z in dom (.: R) & Y = (.: R) . z ) by A4, FUNCT_1:8;
then Y = Im R,x by A5, Def3;
hence y in Y by A1, A5; :: thesis: verum

end;

hence y in R .:^ X by A2, A3, SETFAM_1:def 1; :: thesis: verum

end;

end;