let X be set ; :: thesis: ex Y being set st
( card X c= card Y & X /\ Y = {} )
set D = (bool X) /\ X;
set Y = (bool X) \ ((bool X) /\ X);

C: now :: thesis: not ((bool X) \ ((bool X) /\ X)) /\ X <> {}

assume H: ((bool X) \ ((bool X) /\ X)) /\ X <> {} ; :: thesis: contradiction
set o = the Element of ((bool X) \ ((bool X) /\ X)) /\ X;
H1: ( the Element of ((bool X) \ ((bool X) /\ X)) /\ X in (bool X) \ ((bool X) /\ X) & the Element of ((bool X) \ ((bool X) /\ X)) /\ X in X ) by H, XBOOLE_0:def 4;
then ( the Element of ((bool X) \ ((bool X) /\ X)) /\ X in bool X & not the Element of ((bool X) \ ((bool X) /\ X)) /\ X in (bool X) /\ X ) by XBOOLE_0:def 5;
hence contradiction by H1, XBOOLE_0:def 4; :: thesis: verum

end;

B: card (bool X) c= (card ((bool X) \ ((bool X) /\ X))) +` (card X)

proof

now :: thesis: for o being object st o in bool X holds
o in ((bool X) \ ((bool X) /\ X)) \/ X

let o be object ; :: thesis: ( o in bool X implies b₁ in ((bool X) \ ((bool X) /\ X)) \/ X )
assume B1: o in bool X ; :: thesis: b₁ in ((bool X) \ ((bool X) /\ X)) \/ X

per cases ( o in X or not o in X ) ;

suppose o in X ; :: thesis: b₁ in ((bool X) \ ((bool X) /\ X)) \/ X

hence o in ((bool X) \ ((bool X) /\ X)) \/ X by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not o in X ; :: thesis: b₁ in ((bool X) \ ((bool X) /\ X)) \/ X

then not o in (bool X) /\ X by XBOOLE_0:def 4;
then o in (bool X) \ ((bool X) /\ X) by B1, XBOOLE_0:def 5;
hence o in ((bool X) \ ((bool X) /\ X)) \/ X by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then B1: bool X c= ((bool X) \ ((bool X) /\ X)) \/ X ;
card (((bool X) \ ((bool X) /\ X)) \/ X) = (card ((bool X) \ ((bool X) /\ X))) +` (card X) by C, CARD_2:35, XBOOLE_0:def 7;
hence card (bool X) c= (card ((bool X) \ ((bool X) /\ X))) +` (card X) by B1, CARD_1:11; :: thesis: verum

end;

per cases ( card X = 0 or card X = 1 or card X = 2 or ( card X is finite & card X <> 0 & card X <> 1 & card X <> 2 ) or not card X is finite ) ;

suppose AS: card X = 0 ; :: thesis: ex Y being set st
( card X c= card Y & X /\ Y = {} )

set u = the object ;
take Y = { the object }; :: thesis: ( card X c= card Y & X /\ Y = {} )
thus card X c= card Y by AS; :: thesis: X /\ Y = {}

now :: thesis: not X /\ Y <> {}

assume A: X /\ Y <> {} ; :: thesis: contradiction
set o = the Element of X /\ Y;
( the Element of X /\ Y in X & the Element of X /\ Y in Y ) by A, XBOOLE_0:def 4;
hence contradiction by AS; :: thesis: verum

end;

hence X /\ Y = {} ; :: thesis: verum

end;

suppose AS: card X = 1 ; :: thesis: ex Y being set st
( card X c= card Y & X /\ Y = {} )

then consider o being object such that
A: X = {o} by CARD_2:42;
consider u being object such that
B: not u in {o} by th1;
take Y = {u}; :: thesis: ( card X c= card Y & X /\ Y = {} )
thus card X c= card Y by AS, CARD_2:42; :: thesis: X /\ Y = {}

now :: thesis: not X /\ Y <> {}

assume C: X /\ Y <> {} ; :: thesis: contradiction
set x = the Element of X /\ Y;
( the Element of X /\ Y in X & the Element of X /\ Y in Y ) by C, XBOOLE_0:def 4;
hence contradiction by A, B, TARSKI:def 1; :: thesis: verum

end;

hence X /\ Y = {} ; :: thesis: verum

end;

suppose AS: card X = 2 ; :: thesis: ex Y being set st
( card X c= card Y & X /\ Y = {} )

then consider x, y being object such that
A: ( x <> y & X = {x,y} ) by CARD_2:60;
consider u being object such that
B: not u in {x,y} by th1;
consider v being object such that
C: not v in {x,y,u} by th1;
take Y = {u,v}; :: thesis: ( card X c= card Y & X /\ Y = {} )
u <> v by C, ENUMSET1:def 1;
hence card X c= card Y by AS, CARD_2:57; :: thesis: X /\ Y = {}

now :: thesis: not X /\ Y <> {}

assume H: X /\ Y <> {} ; :: thesis: contradiction
set o = the Element of X /\ Y;
E: ( the Element of X /\ Y in X & the Element of X /\ Y in Y ) by H, XBOOLE_0:def 4;
then F: ( the Element of X /\ Y = x or the Element of X /\ Y = y ) by A, TARSKI:def 2;

per cases ( the Element of X /\ Y = u or the Element of X /\ Y = v ) by E, TARSKI:def 2;

suppose the Element of X /\ Y = u ; :: thesis: contradiction

hence contradiction by A, B, H, XBOOLE_0:def 4; :: thesis: verum

end;

suppose the Element of X /\ Y = v ; :: thesis: contradiction

hence contradiction by F, C, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

hence X /\ Y = {} ; :: thesis: verum

end;

suppose AS: ( card X is finite & card X <> 0 & card X <> 1 & card X <> 2 ) ; :: thesis: ex Y being set st
( card X c= card Y & X /\ Y = {} )

reconsider n = card X as Nat by AS;

D: now :: thesis: not n < 2 + 1

assume n < 2 + 1 ; :: thesis: contradiction
then n <= 2 by NAT_1:13;
then not not n = 0 & ... & not n = 2 ;
hence contradiction by AS; :: thesis: verum

end;

B0: card (bool X) = exp (2,n) by CARD_2:31;

now :: thesis: not card ((bool X) \ ((bool X) /\ X)) c= card X

assume card ((bool X) \ ((bool X) /\ X)) c= card X ; :: thesis: contradiction
then (card ((bool X) \ ((bool X) /\ X))) +` n c= n +` n by CARD_2:83;
then card (bool X) c= n +` n by B;
hence contradiction by D, B0, th0b, CARD_1:4; :: thesis: verum

end;

hence ex Y being set st
( card X c= card Y & X /\ Y = {} ) by C; :: thesis: verum

end;

suppose AS: not card X is finite ; :: thesis: ex Y being set st
( card X c= card Y & X /\ Y = {} )

now :: thesis: not card ((bool X) \ ((bool X) /\ X)) c= card X

assume card ((bool X) \ ((bool X) /\ X)) c= card X ; :: thesis: contradiction
then (card ((bool X) \ ((bool X) /\ X))) +` (card X) c= (card X) +` (card X) by CARD_2:83;
then (card ((bool X) \ ((bool X) /\ X))) +` (card X) c= card X by AS, CARD_2:75;
then card (bool X) c= card X by B;
hence contradiction by CARD_1:4, CARD_1:14; :: thesis: verum

end;

hence ex Y being set st
( card X c= card Y & X /\ Y = {} ) by C; :: thesis: verum

end;

end;