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

proof

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

end;

hence { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P₁[x1,x2,x3] } is Subset of [:X1,X2,X3:] ; :: thesis: verum