let p1, p2, p3 be Prime; :: thesis: ( 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 ) )
assume that
A1: p1,p2,p3 are_mutually_distinct and
A2: ( p1 < 2 or p2 < 3 or p3 < 5 ) and
A3: ( p1 < 2 or p2 < 5 or p3 < 3 ) and
A4: ( p1 < 3 or p2 < 2 or p3 < 5 ) and
A5: ( p1 < 3 or p2 < 5 or p3 < 2 ) and
A6: ( p1 < 5 or p2 < 2 or p3 < 3 ) and
A7: ( p1 < 5 or p2 < 3 or p3 < 2 ) ; :: thesis: contradiction

per cases ( p1 < 1 + 1 or ( p1 >= 2 & p2 < 3 ) or ( p1 >= 2 & p2 >= 3 & p3 < 5 ) ) by A2;

suppose p1 < 1 + 1 ; :: thesis: contradiction

then p1 <= 1 by NAT_1:13;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

suppose that p1 >= 2 and
A8: p2 < 3 ; :: thesis: contradiction

A9: p2 = 2 by A8, NUMBER03:65;
then p3 = 3 by A1, A4, XPRIMET1:3, NUMBER03:65;
hence contradiction by A1, A6, A9, XPRIMET1:3; :: thesis: verum

end;

suppose that A10: p1 >= 2 and
A11: p2 >= 3 and
A12: p3 < 5 ; :: thesis: contradiction

per cases ( p3 = 2 or p3 = 3 ) by A12, XPRIMET1:3;

suppose A13: p3 = 2 ; :: thesis: contradiction

then p1 = 3 by A1, A7, A11, XPRIMET1:3;
hence contradiction by A1, A5, A13, XPRIMET1:3; :: thesis: verum

end;

suppose p3 = 3 ; :: thesis: contradiction

then p2 = 2 by A1, A3, A10, XPRIMET1:3;
hence contradiction by A11; :: thesis: verum

end;

end;

end;

end;