let n be Nat; :: thesis: ( not n divides 82 or n = 1 or n = 2 or n = 41 or n = 82 )
82 = 2 * 41 ;
hence ( not n divides 82 or n = 1 or n = 2 or n = 41 or n = 82 ) by Lem2, XPRIMES1:2, XPRIMES1:41; :: thesis: verum