let x, S1, S2 be set ; :: thesis: ( x in { [:a,b:] where a is Element of S1 \ {{}}, b is Element of S2 \ {{}} : ( a in S1 \ {{}} & b in S2 \ {{}} ) } iff x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) } )
( x in { [:a,b:] where a is Element of S1 \ {{}}, b is Element of S2 \ {{}} : ( a in S1 \ {{}} & b in S2 \ {{}} ) } iff ex a0 being Element of S1 \ {{}} ex b0 being Element of S2 \ {{}} st
( x = [:a0,b0:] & a0 in S1 \ {{}} & b0 in S2 \ {{}} ) ) ;
then ( x in { [:a,b:] where a is Element of S1 \ {{}}, b is Element of S2 \ {{}} : ( a in S1 \ {{}} & b in S2 \ {{}} ) } iff ex a0 being Element of S1 ex b0 being Element of S2 st
( x = [:a0,b0:] & a0 in S1 \ {{}} & b0 in S2 \ {{}} ) ) ;
hence ( x in { [:a,b:] where a is Element of S1 \ {{}}, b is Element of S2 \ {{}} : ( a in S1 \ {{}} & b in S2 \ {{}} ) } iff x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) } ) ; :: thesis: verum