let p be Prime; :: thesis: ( p < 3 implies p = 2 )
assume p < 3 ; :: thesis: p = 2
then p < 2 + 1 ;
then A1: p <= 2 by NAT_1:13;
1 < p by INT_2:def 4;
then 1 + 1 <= p by NAT_1:13;
hence p = 2 by A1, XXREAL_0:1; :: thesis: verum