reconsider IT = RelStr(# (succ X),(FlatRelat X) #) as non empty RelStr ;
X in {X} by TARSKI:def 1;
then reconsider X = X as Element of IT by XBOOLE_0:def 3;
IT is flat
proof
take X ; :: according to POSET_2:def 1 :: thesis: for x, y being Element of IT holds
( x <= y iff ( x = X or x = y ) )
thus for x, y being Element of IT holds
( x <= y iff ( x = X or x = y ) ) by LemFlatten01, LemFlatten02; :: thesis: verum
end;
hence RelStr(# (succ X),(FlatRelat X) #) is non empty strict chain-complete flat Poset ; :: thesis: verum