consider a, b being Ordinal such that
A1: dom A = a \ b by Def1;
take a ; :: according to ORDINAL6:def 1 :: thesis: dom A c= a
thus dom A c= a by A1; :: thesis: verum