theorem LemmaCard2: :: ROUGHIF1:4

for R being finite 1-sorted
for X, Y being Subset of R st card ((X `) \/ Y) = card ([#] R) holds
(X `) \/ Y = [#] R by CARD_2:102;