let n be Nat; :: thesis: (Segm n) \/ {n} = Segm (n + 1)
n in Segm (n + 1) by NAT_1:45;
then A1: {n} c= Segm (n + 1) by ZFMISC_1:31;
Segm n c= Segm (n + 1) by NAT_1:39, NAT_1:11;
hence (Segm n) \/ {n} c= Segm (n + 1) by A1, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: Segm (n + 1) c= (Segm n) \/ {n}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Segm (n + 1) or x in (Segm n) \/ {n} )
assume A2: x in Segm (n + 1) ; :: thesis: x in (Segm n) \/ {n}
then reconsider x = x as Nat ;

now :: thesis: ( ( x < n & x in Segm n ) or ( x = n & x in {n} ) )

x < n + 1 by A2, NAT_1:44;

per cases then ( x < n or x = n ) by NAT_1:22;

case x < n ; :: thesis: x in Segm n

hence x in Segm n by NAT_1:44; :: thesis: verum

end;

case x = n ; :: thesis: x in {n}

hence x in {n} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence x in (Segm n) \/ {n} by XBOOLE_0:def 3; :: thesis: verum