let X1, X2, X3 be non empty set ; { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[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 : P1[x1,x2,x3] } c= [:X1,X2,X3:]
proof
let a be
object ;
TARSKI:def 3 ( not a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[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 : P1[x1,x2,x3] }
;
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] &
P1[
x1,
x2,
x3] )
;
hence
a in [:X1,X2,X3:]
;
verum
end;
hence
{ [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3] } is Subset of [:X1,X2,X3:]
; verum