let X1, X2 be set ; :: thesis: for S1 being Subset-Family of X1
for S2 being Subset-Family of X2 holds { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } = { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) }
let S1 be Subset-Family of X1; :: thesis: for S2 being Subset-Family of X2 holds { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } = { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) }
let S2 be Subset-Family of X2; :: thesis: { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } = { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) }
thus { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } c= { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) } :: according to XBOOLE_0:def 10 :: thesis: { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) } c= { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } or x in { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) } )
assume x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } ; :: thesis: x in { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) }
then consider a being Element of S1, b being Element of S2 such that
A1: ( x = [:a,b:] & a in S1 & b in S2 ) ;
[:a,b:] c= [:X1,X2:] by A1, ZFMISC_1:96;
hence x in { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) } by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) } or x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } )
assume x in { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) } ; :: thesis: x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) }
then ex s0 being Subset of [:X1,X2:] st
( x = s0 & ex a0, b0 being set st
( a0 in S1 & b0 in S2 & s0 = [:a0,b0:] ) ) ;
hence x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } ; :: thesis: verum