let X1, X2 be non empty set ; :: thesis: for S1 being non empty Subset-Family of X1
for S2 being non empty 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 non empty Subset-Family of X1; :: thesis: for S2 being non empty 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 non empty 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 \ {{}} ) ;
thus 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 consider s0 being Subset of [:X1,X2:] such that
A2: ( x = s0 & ex a0, b0 being set st
( a0 in S1 \ {{}} & b0 in S2 \ {{}} & s0 = [:a0,b0:] ) ) ;
consider a0, b0 being set such that
A3: ( a0 in S1 \ {{}} & b0 in S2 \ {{}} & s0 = [:a0,b0:] ) by A2;
( a0 in S1 & b0 in S2 & s0 = [:a0,b0:] ) by TARSKI:def 3, A3, XBOOLE_1:36;
hence x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) } by A2, A3; :: thesis: verum