let X1 be non empty set ; :: thesis: ( ( for x1 being Element of X1 st P1[x1] holds
P2[x1] ) implies { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } )
assume A1: for x1 being Element of X1 st P1[x1] holds
P2[x1] ; :: thesis: { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] }
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { y1 where y1 is Element of X1 : P1[y1] } or a in { z1 where z1 is Element of X1 : P2[z1] } )
assume a in { x1 where x1 is Element of X1 : P1[x1] } ; :: thesis: a in { z1 where z1 is Element of X1 : P2[z1] }
then consider x1 being Element of X1 such that
A2: a = x1 and
A3: P1[x1] ;
 P2[x1] by A1, A3;
hence a in { z1 where z1 is Element of X1 : P2[z1] } by A2; :: thesis: verum