let k, n be Nat; :: thesis: ( k < n implies n \/ {k} = n )
assume k < n ; :: thesis: n \/ {k} = n
then k in Segm n by NAT_1:44;
then {k} c= n by ZFMISC_1:31;
hence n \/ {k} = n by XBOOLE_1:12; :: thesis: verum