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 \ {{}} ) } = { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) }
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 \ {{}} ) } = { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) }
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 \ {{}} ) } = { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) }
for x0 being object holds
( x0 in { [:a,b:] where a is Element of S1 \ {{}}, b is Element of S2 \ {{}} : ( a in S1 \ {{}} & b in S2 \ {{}} ) } iff x0 in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) } )
by Lem7;
hence
{ [:a,b:] where a is Element of S1 \ {{}}, b is Element of S2 \ {{}} : ( a in S1 \ {{}} & b in S2 \ {{}} ) } = { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) }
by TARSKI:2; verum