let n be Nat; :: thesis: ( n is even & n > 4 implies (2 |^ n) - 1 is having_at_least_three_different_divisors )
assume n is even ; :: thesis: ( not n > 4 or (2 |^ n) - 1 is having_at_least_three_different_divisors )
then consider k being Nat such that
A1: n = 2 * k ;
assume that
A2: n > 4 and
A3: not (2 |^ n) - 1 is having_at_least_three_different_divisors ; :: thesis: contradiction
reconsider k = k as non zero Nat by A1, A2;

A4: now :: thesis: not (2 |^ k) - 1 <= 1

assume (2 |^ k) - 1 <= 1 ; :: thesis: contradiction
then ( (2 |^ k) - 1 = 0 or (2 |^ k) - 1 = 1 ) by NAT_1:25;
then 2 |^ k = 2 |^ 1 ;
then k = 1 by PEPIN:30;
hence contradiction by A1, A2; :: thesis: verum

end;

2 |^ (2 * k) = (2 |^ k) |^ 2 by NEWTON:9
.= (2 |^ k) ^2 by WSIERP_1:1 ;
then A5: (2 |^ n) - 1 = ((2 |^ k) + 1) * ((2 |^ k) - 1) by A1;
then A6: (2 |^ k) - 1 divides (2 |^ n) - 1 ;
A7: (2 |^ k) + 1 divides (2 |^ n) - 1 by A5;
A8: (2 |^ k) - 1 < (2 |^ k) + 1 by XREAL_1:8;
then A9: (2 |^ k) + 1 > 1 by A4, XXREAL_0:2;

now :: thesis: ( (2 |^ k) + 1 is prime & (2 |^ k) - 1 is prime )

assume ( not (2 |^ k) + 1 is prime or not (2 |^ k) - 1 is prime ) ; :: thesis: contradiction

per cases then ( not (2 |^ k) - 1 is prime or not (2 |^ k) + 1 is prime ) ;

suppose not (2 |^ k) - 1 is prime ; :: thesis: contradiction

then consider a being Nat such that
A10: a divides (2 |^ k) - 1 and
A11: a <> 1 and
A12: a <> (2 |^ k) - 1 by A4;

A13: now :: thesis: not a <= 1

assume a <= 1 ; :: thesis: contradiction
then ( a = 0 or a = 1 ) by NAT_1:25;
hence contradiction by A10, A11; :: thesis: verum

end;

A14: a,(2 |^ k) - 1,(2 |^ k) + 1 are_mutually_distinct by A8, A10, A12, NAT_D:7;
a divides (2 |^ n) - 1 by A6, A10, INT_2:9;
hence contradiction by A3, A4, A6, A7, A9, A13, A14; :: thesis: verum

end;

suppose not (2 |^ k) + 1 is prime ; :: thesis: contradiction

then consider a being Nat such that
A15: a divides (2 |^ k) + 1 and
A16: a <> 1 and
A17: a <> (2 |^ k) + 1 by A4, A8, XXREAL_0:2;

A18: now :: thesis: not a <= 1

assume a <= 1 ; :: thesis: contradiction
then ( a = 0 or a = 1 ) by NAT_1:25;
hence contradiction by A15, A16; :: thesis: verum

end;

now :: thesis: not a = (2 |^ k) - 1

assume a = (2 |^ k) - 1 ; :: thesis: contradiction
then (2 |^ k) - 1 divides ((2 |^ k) + 1) - ((2 |^ k) - 1) by A15, INT_5:1;
hence contradiction by A4, NUMBER07:9; :: thesis: verum

end;

then A19: a,(2 |^ k) - 1,(2 |^ k) + 1 are_mutually_distinct by A17;
a divides (2 |^ n) - 1 by A7, A15, INT_2:9;
hence contradiction by A3, A4, A6, A7, A9, A18, A19; :: thesis: verum

end;

end;

end;

then k = 2 by Th22;
hence contradiction by A1, A2; :: thesis: verum