let n be Nat; :: thesis: ( not n divides 36 or n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 9 or n = 12 or n = 18 or n = 36 )
assume n divides 36 ; :: thesis: ( n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 9 or n = 12 or n = 18 or n = 36 )
then n divides 6 * 6 ;
then consider a, b being Nat such that
A1: ( a divides 6 & b divides 6 ) and
A2: n = a * b by Lem1;
( ( a = 1 or a = 2 or a = 3 or a = 6 ) & ( b = 1 or b = 2 or b = 3 or b = 6 ) ) by A1, Th10;
hence ( n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 9 or n = 12 or n = 18 or n = 36 ) by A2; :: thesis: verum