let X, Y be set ; :: thesis: for f being Function of X,Y
for SF1, SF2 being Subset-Family of X st SF1 c= SF2 holds
f .: SF1 c= f .: SF2
let f be Function of X,Y; :: thesis: for SF1, SF2 being Subset-Family of X st SF1 c= SF2 holds
f .: SF1 c= f .: SF2
let SF1, SF2 be Subset-Family of X; :: thesis: ( SF1 c= SF2 implies f .: SF1 c= f .: SF2 )
assume A1: SF1 c= SF2 ; :: thesis: f .: SF1 c= f .: SF2
A2: ( f .: SF1 = { (f .: A) where A is Subset of X : A in SF1 } & f .: SF2 = { (f .: A) where A is Subset of X : A in SF2 } ) by Thm07;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: SF1 or x in f .: SF2 )
assume x in f .: SF1 ; :: thesis: x in f .: SF2
then consider A being Subset of X such that
A3: x = f .: A and
A4: A in SF1 by A2;
thus x in f .: SF2 by A1, A2, A3, A4; :: thesis: verum