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 } ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (rng x) where x is Element of A : x in A } or 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
A1: ( y = rng x & x in A ) ;
reconsider xb = x as Element of B by A1;
thus y in { (rng x) where x is Element of B : x in B } by A1; :: thesis: verum