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

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

hence
card A in Segm (card X)
by NAT_1:44; :: thesis: verum
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;then (card A) + (card B) >= (card X) + 1 by A3, XREAL_1:7;

hence contradiction by A4, NAT_1:13; :: thesis: verum