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