let X be non empty set ; :: thesis: 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; :: thesis: ( not [x,y] in FlatRelat X or x = X or x = y )
set a = [x,y];
assume [x,y] in FlatRelat X ; :: thesis: ( 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; :: thesis: verum