let j be Element of 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 ( j = 0 or j = 1 or j = 2 or j = 3 ) by NAT_1:27;
hence ( j = 1 or j = 2 or j = 3 ) by A1; :: thesis: verum