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