let p be Prime; :: thesis: 1 in FreeGen p
for i being Prime st i divides 1 holds
i <= p

proof

let i be Prime; :: thesis: ( i divides 1 implies i <= p )
assume i divides 1 ; :: thesis: i <= p
then i = 1 by WSIERP_1:15;
hence i <= p by INT_2:def 4; :: thesis: verum

end;

hence 1 in FreeGen p by FG, MOEBIUS1:22; :: thesis: verum