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