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 A1: f " (f .: A0) c= f " B0 by RELAT_1:143;
A0 c= f " (f .: A0) by Th41;
hence A0 c= f " B0 by A1; :: 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 A2: f .: A0 c= f .: (f " B0) by RELAT_1:123;
f .: (f " B0) c= B0 by FUNCT_1:75;
hence f .: A0 c= B0 by A2; :: thesis: verum

end;