let a be Nat; :: thesis: (Seg a) \/ {(a + 1)} = Seg (a + 1)
thus (Seg a) \/ {(a + 1)} c= Seg (a + 1) :: according to XBOOLE_0:def 10 :: thesis: Seg (a + 1) c= (Seg a) \/ {(a + 1)}

proof

a + 0 <= a + 1 by XREAL_1:9;
then A1: Seg a c= Seg (a + 1) by Th7;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg a) \/ {(a + 1)} or x in Seg (a + 1) )
assume x in (Seg a) \/ {(a + 1)} ; :: thesis: x in Seg (a + 1)
then ( x in Seg a or x in {(a + 1)} ) by XBOOLE_0:def 3;
then ( x in Seg (a + 1) or x = a + 1 ) by A1, TARSKI:def 1;
hence x in Seg (a + 1) by Th5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (a + 1) or x in (Seg a) \/ {(a + 1)} )
assume A2: x in Seg (a + 1) ; :: thesis: x in (Seg a) \/ {(a + 1)}
then reconsider x = x as Element of NAT ;
( 1 <= x & x <= a + 1 ) by A2, Th3;
then ( 1 <= x & ( x <= a or x = a + 1 ) ) by NAT_1:8;
then ( x in Seg a or x in {(a + 1)} ) by TARSKI:def 1;
hence x in (Seg a) \/ {(a + 1)} by XBOOLE_0:def 3; :: thesis: verum