let X1, X2, X3 be non empty set ; [:X1,X2,X3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum }
defpred S1[ set , set , set ] means verum;
A1:
for x being Element of [:X1,X2,X3:] holds x in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum }
proof
let x be
Element of
[:X1,X2,X3:];
x in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum }
x = [(x `1_3),(x `2_3),(x `3_3)]
;
hence
x in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum }
;
verum
end;
for X1, X2, X3 being non empty set holds { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : S1[x1,x2,x3] } is Subset of [:X1,X2,X3:]
from DOMAIN_1:sch 3();
then
{ [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum } is Subset of [:X1,X2,X3:]
;
hence
[:X1,X2,X3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum }
by A1, SUBSET_1:28; verum