let T, S be non empty set ; :: thesis: for f being Function of T,S
for A, B being Subset-Family of S st A c= B holds
f " A c= f " B
let f be Function of T,S; :: thesis: for A, B being Subset-Family of S st A c= B holds
f " A c= f " B
let A, B be Subset-Family of S; :: thesis: ( A c= B implies f " A c= f " B )
assume A1: A c= B ; :: thesis: f " A c= f " B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " A or x in f " B )
assume A2: x in f " A ; :: thesis: x in f " B
then reconsider x = x as Subset of T ;
ex C being Subset of S st
( C in B & x = f " C )

proof

consider C being Subset of S such that
A3: ( C in A & x = f " C ) by A2, Def9;
take C ; :: thesis: ( C in B & x = f " C )
thus ( C in B & x = f " C ) by A1, A3; :: thesis: verum

end;

hence x in f " B by Def9; :: thesis: verum