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