let j be Nat; :: thesis: ( 1 <= j & j < 4 & not j = 1 & not j = 2 implies j = 3 )
assume that
A1: 1 <= j and
A2: j < 4 ; :: thesis: ( 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; :: thesis: verum