let m be Element of NAT ; :: thesis: ( not m in Seg 4 or m = 1 or m = 2 or m = 3 or m = 4 )
assume A1: m in Seg 4 ; :: thesis: ( m = 1 or m = 2 or m = 3 or m = 4 )
then ( 1 <= m & m <= 4 ) by FINSEQ_1:3;
then ( m = 0 or m = 1 or m = 2 or m = 3 or m = 4 ) by NAT_1:29;
hence ( m = 1 or m = 2 or m = 3 or m = 4 ) by A1, FINSEQ_1:3; :: thesis: verum