let R be finite set ; :: thesis: for X, Y being Subset of R holds
( card (X \/ Y) = card (X /\ Y) iff X = Y )
let X, Y be Subset of R; :: thesis: ( card (X \/ Y) = card (X /\ Y) iff X = Y )
hereby :: thesis: ( X = Y implies card (X \/ Y) = card (X /\ Y) )
assume card (X \/ Y) = card (X /\ Y) ; :: thesis: X = Y
then A2: X /\ Y = X \/ Y by CARD_2:102, XBOOLE_1:29;
then X = X \/ (X \/ Y) by XBOOLE_1:22;
then X = X \/ Y by XBOOLE_1:6;
hence X = Y by XBOOLE_1:21, A2; :: thesis: verum
end;
assume X = Y ; :: thesis: card (X \/ Y) = card (X /\ Y)
hence card (X \/ Y) = card (X /\ Y) ; :: thesis: verum