for X being non empty set
for x, y being Element of succ X holds
( [x,y] in FlatRelat X iff ( x = X or x = y ) ) by LemFlatten01, LemFlatten02;