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
hence card x c= n + 1 by Lnatmost; :: thesis: verum