let x be set ; :: according to SCMYCIEL:def 4 :: thesis: ( x in X \/ Y implies card x c= n + 1 )
assume A: x in X \/ Y ; :: thesis: card x c= n + 1
( x in X or x in Y ) by A, XBOOLE_0:def 3;
hence card x c= n + 1 by Lnatmost; :: thesis: verum