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