let R be finite 1-sorted ; :: thesis: for X, Y being Subset of R holds
( card (X \/ Y) = card Y iff X c= Y )
let X, Y be Subset of R; :: thesis: ( card (X \/ Y) = card Y iff X c= Y )
( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
hence ( card (X \/ Y) = card Y implies X c= Y ) by CARD_2:102; :: thesis: ( X c= Y implies card (X \/ Y) = card Y )
assume X c= Y ; :: thesis: card (X \/ Y) = card Y
hence card (X \/ Y) = card Y by XBOOLE_1:12; :: thesis: verum