let X1, X2, X3, X4 be non empty set ; :: thesis: for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }
let A1 be Subset of X1; :: thesis: for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }
let A2 be Subset of X2; :: thesis: for A3 being Subset of X3
for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }
let A3 be Subset of X3; :: thesis: for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }
let A4 be Subset of X4; :: thesis: [:A1,A2,A3,A4:] = { [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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }
thus [:A1,A2,A3,A4:] c= { [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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } :: according to XBOOLE_0:def 10 :: 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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } c= [:A1,A2,A3,A4:]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [:A1,A2,A3,A4:] or 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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } )
assume A1: a in [:A1,A2,A3,A4:] ; :: thesis: 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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }
reconsider A1 = A1 as non empty Subset of X1 by A1, MCART_1:51;
reconsider A2 = A2 as non empty Subset of X2 by A1, MCART_1:51;
reconsider A3 = A3 as non empty Subset of X3 by A1, MCART_1:51;
reconsider A4 = A4 as non empty Subset of X4 by A1, MCART_1:51;
A2: a in [:A1,A2,A3,A4:] by A1;
then reconsider x = a as Element of [:X1,X2,X3,X4:] ;
A3: ( x `3_4 in A3 & x `4_4 in A4 ) by A2, MCART_1:83;
A4: x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
( x `1_4 in A1 & x `2_4 in A2 ) by A2, MCART_1:83;
hence 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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } by A4, A3; :: thesis: verum

end;

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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } or a in [:A1,A2,A3,A4:] )
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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) } ; :: thesis: a in [:A1,A2,A3,A4:]
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] & x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) ;
hence a in [:A1,A2,A3,A4:] by MCART_1:80; :: thesis: verum