let a be natural Ordinal; :: thesis: ( a hcf a = a & a lcm a = a )
reconsider c = a as Element of omega by ORDINAL1:def 12;
for b being natural Ordinal st b divides a & b divides a holds
b divides c ;
hence a hcf a = a by Def5; :: thesis: a lcm a = a
for b being natural Ordinal st a divides b & a divides b holds
c divides b ;
hence a lcm a = a by Def4; :: thesis: verum