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

proof

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

end;

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