let X be non empty set ; :: thesis: for x, y being Element of succ X st ( x = X or x = y ) holds
[x,y] in FlatRelat X
let x, y be Element of succ X; :: thesis: ( ( x = X or x = y ) implies [x,y] in FlatRelat X )
assume A1: ( x = X or x = y ) ; :: thesis: [x,y] in FlatRelat X
A2: ( x in {X} or x in X ) by XBOOLE_0:def 3;
A3: ( y in {X} or y in X ) by XBOOLE_0:def 3;
set a = [x,y];

per cases ( x = X or x = y ) by A1;

suppose B1: x = X ; :: thesis: [x,y] in FlatRelat X

per cases ( y = X or y <> X ) ;

suppose y = X ; :: thesis: [x,y] in FlatRelat X

then [x,y] in {[X,X]} by B1, TARSKI:def 1;
hence [x,y] in FlatRelat X by LemSUM01; :: thesis: verum

end;

suppose y <> X ; :: thesis: [x,y] in FlatRelat X

then [x,y] in [:{X},X:] by B1, ZFMISC_1:105, A3, TARSKI:def 1;
hence [x,y] in FlatRelat X by LemSUM01; :: thesis: verum

end;

end;

end;

suppose B2: x = y ; :: thesis: [x,y] in FlatRelat X

per cases ( x = X or x <> X ) ;

suppose x = X ; :: thesis: [x,y] in FlatRelat X

then [x,y] in {[X,X]} by B2, TARSKI:def 1;
hence [x,y] in FlatRelat X by LemSUM01; :: thesis: verum

end;

suppose x <> X ; :: thesis: [x,y] in FlatRelat X

then [x,y] in id X by B2, RELAT_1:def 10, A2, TARSKI:def 1;
hence [x,y] in FlatRelat X by LemSUM01; :: thesis: verum

end;

end;

end;

end;