assume A1: for n being Nat st n > 5 holds
ex p, q being Prime st
( n < p & p < q & q < 2 * n ) ; :: thesis: for n being Nat st n > 10 holds
ex p, q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 )
let n be Nat; :: thesis: ( n > 10 implies ex p, q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 ) )
assume A2: n > 10 ; :: thesis: ex p, q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 )
n >= 10 + 1 by A2, NAT_1:13;

per cases then ( n = 11 or n > 11 ) by XXREAL_0:1;

suppose A3: n = 11 ; :: thesis: ex p, q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 )

reconsider p = 7, q = 11 as Prime by XPRIMES1:7, XPRIMES1:11;
take p ; :: thesis: ex q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 )
take q ; :: thesis: ( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 )
1 div 2 = 0 by NAT_D:27;
then A4: ((5 * 2) + 1) div 2 = 5 + 0 by NAT_D:61;
A5: q |^ 1 divides q ! by NEWTON:41;
2 * 11 > 11 ;
then not q |^ (1 + 1) divides q ! by Th36;
hence ( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 ) by A4, Th38, A3, A5, NAT_3:def 7; :: thesis: verum

end;

suppose n > 11 ; :: thesis: ex p, q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 )

then A6: n >= 11 + 1 by NAT_1:13;
set k = n div 2;
(6 * 2) div 2 = 6 by NAT_D:18;
then 5 + 1 <= n div 2 by A6, NAT_2:24;
then 5 < n div 2 by NAT_1:13;
then consider p, q being Prime such that
A7: ( n div 2 < p & p < q & q < 2 * (n div 2) ) by A1;
take p ; :: thesis: ex q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 )
take q ; :: thesis: ( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 )
( p <= 2 * (n div 2) & n div 2 < q & 2 < n ) by A2, A7, XXREAL_0:2;
hence ( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 ) by A7, Th38; :: thesis: verum

end;

end;