let X1, X2 be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: [: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 ) } :: according to XBOOLE_0:def 10 :: thesis: { [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 set ; :: according to TARSKI:def 3 :: thesis: ( 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:] ; :: thesis: 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:] ;
( x = [(x `1 ),(x `2 )] & x `1 in A1 & x `2 in A2 ) by A1, MCART_1:10, MCART_1:23;
hence a in { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) } ; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( 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 ) } ; :: thesis: 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:106; :: thesis: verum