let X1, X2, X3, X4 be non empty set ; 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; 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; 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; 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; [: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 ) }
XBOOLE_0:def 10 { [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 ;
TARSKI:def 3 ( 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:]
;
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;
verum
end;
let a be object ; TARSKI:def 3 ( 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 ) }
; 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; verum