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 m <= 4 by FINSEQ_1:1;
then not not m = 0 & ... & not m = 4 by NAT_1:60;
hence ( m = 1 or m = 2 or m = 3 or m = 4 ) by A1, FINSEQ_1:1; :: thesis: verum