let X be non empty set ; for x, y being Element of succ X holds
( not [x,y] in FlatRelat X or x = X or x = y )
let x, y be Element of succ X; ( not [x,y] in FlatRelat X or x = X or x = y )
set a = [x,y];
assume
[x,y] in FlatRelat X
; ( x = X or x = y )
then
( [x,y] in {[X,X]} or [x,y] in [:{X},X:] or [x,y] in id X )
by LemSUM01;
then
( [x,y] = [X,X] or x = X or x = y )
by TARSKI:def 1, ZFMISC_1:105, RELAT_1:def 10;
hence
( x = X or x = y )
by XTUPLE_0:1; verum