let X1, X2 be set ; :: thesis: for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2 holds { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } = { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum }
let S1 be non empty Subset-Family of X1; :: thesis: for S2 being non empty Subset-Family of X2 holds { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } = { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum }
let S2 be non empty Subset-Family of X2; :: thesis: { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } = { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum }
A1: for x being object st x in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } holds
x in { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum }

proof

let x be object ; :: thesis: ( x in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } implies x in { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum } )
assume x in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } ; :: thesis: x in { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum }
then ex s being Subset of [:X1,X2:] st
( x = s & ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) ) ;
hence x in { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum } ; :: thesis: verum

end;

for x being object st x in { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum } holds
x in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) }

proof

let x be object ; :: thesis: ( x in { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum } implies x in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } )
assume x in { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum } ; :: thesis: x in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) }
then ex x1 being Element of S1 ex x2 being Element of S2 st x = [:x1,x2:] ;
hence x in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } ; :: thesis: verum

end;

hence { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } = { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum } by A1, TARSKI:2; :: thesis: verum