let X1, X2 be non empty set ; 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; 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; { [: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:] ) }
XBOOLE_0:def 10 { 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 ;
TARSKI:def 3 ( 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 \ {{}} ) }
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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:] ) }
; 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; verum