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