theorem Th49: :: NUMBER08:49

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