let A, B be non empty set ; :: thesis: for f being Function of A,B
for A0 being Subset of A
for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )
let f be Function of A,B; :: thesis: for A0 being Subset of A
for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )
let A0 be Subset of A; :: thesis: for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )
let B0 be Subset of B; :: thesis: ( f .: A0 c= B0 iff A0 c= f " B0 )
thus ( f .: A0 c= B0 implies A0 c= f " B0 ) :: thesis: ( A0 c= f " B0 implies f .: A0 c= B0 )

proof

assume f .: A0 c= B0 ; :: thesis: A0 c= f " B0
then ( f " (f .: A0) c= f " B0 & A0 c= f " (f .: A0) ) by Th50, RELAT_1:178;
hence A0 c= f " B0 by XBOOLE_1:1; :: thesis: verum

end;

thus ( A0 c= f " B0 implies f .: A0 c= B0 ) :: thesis: verum

proof

assume A0 c= f " B0 ; :: thesis: f .: A0 c= B0
then ( f .: A0 c= f .: (f " B0) & f .: (f " B0) c= B0 ) by FUNCT_1:145, RELAT_1:156;
hence f .: A0 c= B0 by XBOOLE_1:1; :: thesis: verum

end;