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