let n be Nat; ( not n divides 50 or n = 1 or n = 2 or n = 5 or n = 10 or n = 25 or n = 50 )
assume
n divides 50
; ( n = 1 or n = 2 or n = 5 or n = 10 or n = 25 or n = 50 )
then
n divides 2 * 25
;
then consider a, b being Nat such that
A1:
( a divides 2 & b divides 25 )
and
A2:
n = a * b
by Lem1;
( ( a = 1 or a = 2 ) & ( b = 1 or b = 5 or b = 25 ) )
by A1, Th9, Th13;
hence
( n = 1 or n = 2 or n = 5 or n = 10 or n = 25 or n = 50 )
by A2; verum