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