let j be Element of NAT ; :: thesis: ( 1 <= j & j < 4 & not j = 1 & not j = 2 implies j = 3 )
assume A1: ( 1 <= j & j < 4 ) ; :: thesis: ( j = 1 or j = 2 or j = 3 )
then j < 3 + 1 ;
then j <= 3 by NAT_1:13;
then ( j = 0 or j = 1 or j = 2 or j = 3 ) by NAT_1:28;
hence ( j = 1 or j = 2 or j = 3 ) by A1; :: thesis: verum