let X1, X2 be non empty set ; for A1 being Subset of X1
for A2 being Subset of X2 holds [:A1,A2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) }
let A1 be Subset of X1; for A2 being Subset of X2 holds [:A1,A2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) }
let A2 be Subset of X2; [:A1,A2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) }
thus
[:A1,A2:] c= { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) }
XBOOLE_0:def 10 { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } c= [:A1,A2:]proof
let a be
object ;
TARSKI:def 3 ( not a in [:A1,A2:] or a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } )
assume A1:
a in [:A1,A2:]
;
a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) }
then reconsider x =
a as
Element of
[:X1,X2:] ;
A2:
x = [(x `1),(x `2)]
;
(
x `1 in A1 &
x `2 in A2 )
by A1, MCART_1:10;
hence
a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) }
by A2;
verum
end;
let a be object ; TARSKI:def 3 ( not a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } or a in [:A1,A2:] )
assume
a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) }
; a in [:A1,A2:]
then
ex x1 being Element of X1 ex x2 being Element of X2 st
( a = [x1,x2] & x1 in A1 & x2 in A2 )
;
hence
a in [:A1,A2:]
by ZFMISC_1:87; verum