let n be Element of NAT ; :: thesis: ( 1 < n & n < 5 & n is prime & not n = 2 implies n = 3 )
assume A1: ( 1 < n & n < 5 & n is prime ) ; :: thesis: ( n = 2 or n = 3 )
then ( 1 + 1 < n + 1 & n < 4 + 1 ) by XREAL_1:8;
then ( ( 2 <= n & n <= 2 + 1 ) or ( 3 <= n & n <= 3 + 1 ) ) by NAT_1:13;
hence ( n = 2 or n = 3 ) by A1, INT_2:46, NAT_1:9; :: thesis: verum