let X be non empty set ; :: thesis: { [A,B] where A, B is Element of X : ( B = {} implies A = {} ) } = [:X,X:] \ [:(X \ {{}}),{{}}:]

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:X,X:] \ [:(X \ {{}}),{{}}:] c= { [A,B] where A, B is Element of X : ( B = {} implies A = {} ) }

let o be object ; :: thesis: ( o in { [A,B] where A, B is Element of X : ( B = {} implies A = {} ) } implies o in [:X,X:] \ [:(X \ {{}}),{{}}:] )
assume o in { [A,B] where A, B is Element of X : ( B = {} implies A = {} ) } ; :: thesis: o in [:X,X:] \ [:(X \ {{}}),{{}}:]
then consider A, B being Element of X such that
A1: o = [A,B] and
A2: ( B = {} implies A = {} ) ;
A3: o in [:X,X:] by A1, ZFMISC_1:def 2;

now :: thesis: not o in [:(X \ {{}}),{{}}:]

assume o in [:(X \ {{}}),{{}}:] ; :: thesis: contradiction
then ex a, b being object st
( a in X \ {{}} & b in {{}} & o = [a,b] ) by ZFMISC_1:def 2;
hence contradiction by A1, A2, XTUPLE_0:1; :: thesis: verum

end;

hence o in [:X,X:] \ [:(X \ {{}}),{{}}:] by A3, XBOOLE_0:def 5; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in [:X,X:] \ [:(X \ {{}}),{{}}:] or o in { [A,B] where A, B is Element of X : ( B = {} implies A = {} ) } )
assume A4: o in [:X,X:] \ [:(X \ {{}}),{{}}:] ; :: thesis: o in { [A,B] where A, B is Element of X : ( B = {} implies A = {} ) }
then ( o in [:X,X:] & not o in [:(X \ {{}}),{{}}:] ) by XBOOLE_0:def 5;
then consider u, v being object such that
A5: u in X and
A6: v in X and
A7: o = [u,v] by ZFMISC_1:def 2;
reconsider u = u, v = v as Element of X by A5, A6;
not [u,v] in [:(X \ {{}}),{{}}:] by A7, A4, XBOOLE_0:def 5;
then ( not u in X \ {{}} or not v in {{}} ) by ZFMISC_1:def 2;
then ( not u in X or u in {{}} or not v in {{}} ) by XBOOLE_0:def 5;
then ( not u in X or u = {} or not v = {} ) by TARSKI:def 1;
hence o in { [A,B] where A, B is Element of X : ( B = {} implies A = {} ) } by A5, A6, A7; :: thesis: verum