let p be Prime; :: thesis: ( p + 2 is Prime & p + 6 is Prime & p + 8 is Prime & p + 12 is Prime & p + 14 is Prime implies p = 5 )
assume A1: ( p + 2 is Prime & p + 6 is Prime & p + 8 is Prime & p + 12 is Prime & p + 14 is Prime ) ; :: thesis: p = 5
assume FF: p <> 5 ; :: thesis: contradiction
consider k being Nat such that
ZZ: ( p = 5 * k or p = (5 * k) + 1 or p = (5 * k) + 2 or p = (5 * k) + 3 or p = (5 * k) + 4 ) by NUMBER02:25;

per cases ( p = 5 * k or p = (5 * k) + 1 or p = (5 * k) + 2 or p = (5 * k) + 3 or p = (5 * k) + 4 ) by ZZ;

suppose S1: p = 5 * k ; :: thesis: contradiction

S2: k <> 0 by S1;
k <> 1 by FF, S1;
then reconsider k = k as non trivial non zero Nat by S2, NAT_2:def 1;
5 * k is composite by XPRIMES1:5;
hence contradiction by S1; :: thesis: verum

end;

suppose p = (5 * k) + 1 ; :: thesis: contradiction

then p + 14 = 5 * (k + 3) ;
hence contradiction by A1, XPRIMES1:5; :: thesis: verum

end;

suppose p = (5 * k) + 2 ; :: thesis: contradiction

then p + 8 = 5 * (k + 2) ;
hence contradiction by A1, XPRIMES1:5; :: thesis: verum

end;

suppose p = (5 * k) + 3 ; :: thesis: contradiction

then p + 12 = 5 * (k + 3) ;
hence contradiction by A1, XPRIMES1:5; :: thesis: verum

end;

suppose S1: p = (5 * k) + 4 ; :: thesis: contradiction

p + 6 = 5 * (k + 2) by S1;
hence contradiction by A1, XPRIMES1:5; :: thesis: verum

end;

end;