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