let X be non empty finite set ; :: thesis: for A, B being non empty set st X = A \/ B & A misses B holds
card A in card X
let A, B be non empty set ; :: thesis: ( X = A \/ B & A misses B implies card A in card X )
set n = card X;
assume A1: ( X = A \/ B & A misses B ) ; :: thesis: card A in card X
then A2: ( card A c= card X & card B c= card X ) by CARD_1:27, XBOOLE_1:7;
then reconsider A = A as finite set ;
reconsider B = B as finite set by A2;
A3: card X = (card A) + (card B) by A1, CARD_2:53;
A4: ( card A >= 1 & card B >= 1 ) by NAT_1:14;
A5: card A < card X

proof

assume not card A < card X ; :: thesis: contradiction
then (card A) + (card B) >= (card X) + 1 by A4, XREAL_1:9;
hence contradiction by A3, NAT_1:13; :: thesis: verum

end;

thus card A in card X by A5, NAT_1:45; :: thesis: verum