let T, S be set ; :: thesis: for f being Function of T,S
for A, B being Subset-Family of T 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 T st A c= B holds
f .: A c= f .: B
let A, B be Subset-Family of T; :: 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 S ;
ex C being Subset of T st
( C in B & x = f .: C )

proof

consider C being Subset of T such that
A3: ( C in A & x = f .: C ) by A2, Def10;
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 Def10; :: thesis: verum