let U be Universe; :: thesis: [:U,U:] \ [:(U \ {{}}),{{}}:] is not Element of U
assume A1: [:U,U:] \ [:(U \ {{}}),{{}}:] is Element of U ; :: thesis: contradiction
reconsider x = {{}} as Element of U by CLASSES2:56, CLASSES2:57;

now :: thesis: for o being object st o in [:U,{x}:] holds
o in [:U,U:] \ [:(U \ {{}}),{{}}:]

let o be object ; :: thesis: ( o in [:U,{x}:] implies o in [:U,U:] \ [:(U \ {{}}),{{}}:] )
assume o in [:U,{x}:] ; :: thesis: o in [:U,U:] \ [:(U \ {{}}),{{}}:]
then consider a, b being object such that
A2: a in U and
A3: b in {x} and
A4: o = [a,b] by ZFMISC_1:def 2;

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

b = x by A3, TARSKI:def 1;
hence o in [:U,U:] by A2, A4, ZFMISC_1:def 2; :: thesis: not o in [:(U \ {{}}),{{}}:]

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

assume o in [:(U \ {{}}),{{}}:] ; :: thesis: contradiction
then consider c, d being object such that
c in U \ {{}} and
A5: d in {{}} and
A6: o = [c,d] by ZFMISC_1:def 2;
( c = a & b = d ) by A4, A6, XTUPLE_0:1;
hence contradiction by A3, A5, TARSKI:def 1; :: thesis: verum

end;

hence not o in [:(U \ {{}}),{{}}:] ; :: thesis: verum

end;

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

end;

then ( [:U,{x}:] c= [:U,U:] \ [:(U \ {{}}),{{}}:] & [:U,U:] \ [:(U \ {{}}),{{}}:] in U ) by A1;
then [:U,{x}:] in U by CLASSES4:13;
then proj1 [:U,{x}:] is Element of U by CLASSES4:36;
then U in U ;
hence contradiction ; :: thesis: verum