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 Segm (card X)
let A, B be non empty set ; :: thesis: ( X = A \/ B & A misses B implies card A in Segm (card X) )
set n = card X;
assume that
A1: X = A \/ B and
A2: A misses B ; :: thesis: card A in Segm (card X)
card B c= card X by A1, CARD_1:11, XBOOLE_1:7;
then reconsider B = B as finite set ;
card A c= card X by A1, CARD_1:11, XBOOLE_1:7;
then reconsider A = A as finite set ;
A3: card B >= 1 by NAT_1:14;
A4: card X = (card A) + (card B) by A1, A2, CARD_2:40;
card A < card X

proof

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

end;

hence card A in Segm (card X) by NAT_1:44; :: thesis: verum