let a be natural Number ; :: 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:7;
then A1: Seg a c= Seg (a + 1) by Th5;
let x be object ; :: 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 Th3; :: thesis: verum

end;

let x be object ; :: 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 ;
A3: x <= a + 1 by A2, Th1;
A4: 1 <= x by A2, Th1;
( x <= a or x = a + 1 ) by A3, NAT_1:8;
then ( x in Seg a or x in {(a + 1)} ) by A4, TARSKI:def 1;
hence x in (Seg a) \/ {(a + 1)} by XBOOLE_0:def 3; :: thesis: verum