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

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

( 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

set d = b - a;
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;

end;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 )
;

end;

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;.= a by FINSEQ_1:57 ;

hence contradiction by L519, L000, FINSEQ_1:57; :: thesis: verum

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;.= a + 1 by FINSEQ_1:57 ;

hence contradiction by L505, L300; :: thesis: verum

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