let p1, p2 be Prime; :: thesis: ( not p1 <> p2 or ( 2 <= p1 & 3 <= p2 ) or ( 3 <= p1 & 2 <= p2 ) )
assume A1: p1 <> p2 ; :: thesis: ( ( 2 <= p1 & 3 <= p2 ) or ( 3 <= p1 & 2 <= p2 ) )
assume ( 2 > p1 or 3 > p2 ) ; :: thesis: ( 3 <= p1 & 2 <= p2 )

per cases then ( p1 < 1 + 1 or p2 < 3 ) ;

suppose p1 < 1 + 1 ; :: thesis: ( 3 <= p1 & 2 <= p2 )

then p1 <= 1 by NAT_1:13;
hence ( 3 <= p1 & 2 <= p2 ) by INT_2:def 4; :: thesis: verum

end;

suppose A2: p2 < 3 ; :: thesis: ( 3 <= p1 & 2 <= p2 )

1 < p2 by INT_2:def 4;
then A3: 1 + 1 <= p2 by NAT_1:13;
1 < p1 by INT_2:def 4;
then A4: 1 + 1 <= p1 by NAT_1:13;
2 = 3 - 1 ;
then not not p2 = 0 & ... & not p2 = 2 by A2, NUMBER02:7;
then 2 < p1 by A1, A4, INT_2:def 4, XXREAL_0:1;
then 2 + 1 <= p1 by NAT_1:13;
hence ( 3 <= p1 & 2 <= p2 ) by A3; :: thesis: verum

end;

end;