let a, b be Nat; :: thesis: for s being set holds
( not (Seg a) \/ {s} = Seg b or a = b or a + 1 = b )
let s be set ; :: thesis: ( not (Seg a) \/ {s} = Seg b or a = b or a + 1 = b )
assume L000: Seg b = (Seg a) \/ {s} ; :: thesis: ( a = b or a + 1 = b )
then L300: card ((Seg a) \/ {s}) = b by FINSEQ_1:57;
L500: b - a <= 1

proof

assume L505: b - a > 1 ; :: thesis: contradiction
then (b - a) + a > 1 + a by XREAL_1:8;
then L519: b - 0 > (a + 1) - 1 by XREAL_1:14;

per cases ( s in Seg a or not s in Seg a ) ;

suppose s in Seg a ; :: thesis: contradiction

then card ((Seg a) \/ {s}) = card (Seg a) by ZFMISC_1:40
.= a by FINSEQ_1:57 ;
hence contradiction by L519, L000, FINSEQ_1:57; :: thesis: verum

end;

suppose not s in Seg a ; :: thesis: contradiction

then card ((Seg a) \/ {s}) = (card (Seg a)) + 1 by CARD_2:41
.= a + 1 by FINSEQ_1:57 ;
hence contradiction by L505, L300; :: thesis: verum

end;

end;

end;

set d = b - a;
a <= b - 0 by L000, XBOOLE_1:11, FINSEQ_1:5;
then b - a in NAT by XREAL_1:11, INT_1:3;
then reconsider d = b - a as Nat ;
( d = 0 or d = 1 ) by L500, NAT_1:25;
hence ( a = b or a + 1 = b ) ; :: thesis: verum