let j be Nat; ( 1 <= j & j < 4 & not j = 1 & not j = 2 implies j = 3 )
assume that
A1:
1 <= j
and
A2:
j < 4
; ( j = 1 or j = 2 or j = 3 )
j < 3 + 1
by A2;
then
j <= 3
by NAT_1:13;
then
not not j = 0 & ... & not j = 3
by NAT_1:60;
hence
( j = 1 or j = 2 or j = 3 )
by A1; verum