consider a being Ordinal such that
A1: X c= a by Def1;
consider b being Ordinal such that
A2: Y c= b by Def1;
take a \/ b ; :: according to ORDINAL6:def 1 :: thesis: X \/ Y c= a \/ b
thus X \/ Y c= a \/ b by A1, A2, XBOOLE_1:13; :: thesis: verum