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 \ {{}} ) } = { [: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; :: 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 \ {{}} ) } = { [: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; :: thesis: { [: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; :: thesis: verum