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

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