let B be functional set ; :: thesis: for A being Subset of B holds { (rng x) where x is Element of A : x in A } c= { (rng x) where x is Element of B : x in B }
let A be Subset of B; :: thesis: { (rng x) where x is Element of A : x in A } c= { (rng x) where x is Element of B : x in B }
set AF = { (rng x) where x is Element of A : x in A } ;
set BF = { (rng x) where x is Element of B : x in B } ;

now

let y be set ; :: thesis: ( y in { (rng x) where x is Element of A : x in A } implies y in { (rng x) where x is Element of B : x in B } )
assume y in { (rng x) where x is Element of A : x in A } ; :: thesis: y in { (rng x) where x is Element of B : x in B }
then consider x being Element of A such that
C0: ( y = rng x & x in A ) ;
reconsider xb = x as Element of B by C0;
thus y in { (rng x) where x is Element of B : x in B } by C0; :: thesis: verum

end;

hence { (rng x) where x is Element of A : x in A } c= { (rng x) where x is Element of B : x in B } by TARSKI:def 3; :: thesis: verum