let n be Nat; :: thesis: ( n < 5 & n is prime & not n = 2 implies n = 3 )
assume that
A1: n < 5 and
A2: n is prime ; :: thesis: ( n = 2 or n = 3 )
1 < n by A2, INT_2:def 4;
then ( 1 + 1 < n + 1 & n < 4 + 1 ) by A1, XREAL_1:6;
then ( ( 2 <= n & n <= 2 + 1 ) or ( 3 <= n & n <= 3 + 1 ) ) by NAT_1:13;
hence ( n = 2 or n = 3 ) by A2, INT_2:29, NAT_1:9; :: thesis: verum