let X1 be non empty set ; :: thesis: { x1 where x1 is Element of X1 : P₁[x1] } is Subset of X1
{ x1 where x1 is Element of X1 : P₁[x1] } c= X1

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x1 where x1 is Element of X1 : P₁[x1] } or a in X1 )
assume a in { x1 where x1 is Element of X1 : P₁[x1] } ; :: thesis: a in X1
then ex x1 being Element of X1 st
( a = x1 & P₁[x1] ) ;
hence a in X1 ; :: thesis: verum

end;

hence { x1 where x1 is Element of X1 : P₁[x1] } is Subset of X1 ; :: thesis: verum