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