let n be Nat; :: thesis: ( n satisfies_Sierpinski_problem_86 implies n >= 6 )
given a, b, c being Prime such that A1: a,b,c are_mutually_distinct and
A2: (n |^ 2) - 1 = (a * b) * c ; :: according to NUMBER08:def 5 :: thesis: n >= 6
( ( a >= 2 & b >= 3 & c >= 5 ) or ( a >= 2 & b >= 5 & c >= 3 ) or ( a >= 3 & b >= 2 & c >= 5 ) or ( a >= 3 & b >= 5 & c >= 2 ) or ( a >= 5 & b >= 2 & c >= 3 ) or ( a >= 5 & b >= 3 & c >= 2 ) ) by A1, Th49;
then A3: ( (a * b) * c >= (2 * 3) * 5 or (a * b) * c >= (3 * 5) * 2 or (a * b) * c >= (5 * 2) * 3 ) by Lm15;
A4: 5 = 6 - 1 ;
A5: n |^ 2 = n * n by WSIERP_1:1;
assume n < 6 ; :: thesis: contradiction
then not not n = 0 & ... & not n = 5 by A4, NUMBER02:7;
hence contradiction by A2, A3, A5; :: thesis: verum