theorem Th40: :: NUMBER07:40

for p1, p2 being Prime holds
( not p1 <> p2 or ( 2 <= p1 & 3 <= p2 ) or ( 3 <= p1 & 2 <= p2 ) )