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);

( 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 <> {}

B:
card (bool X) c= (card ((bool X) \ ((bool X) /\ X))) +` (card 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;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

proof

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;

now :: thesis: for o being object st o in bool X holds

o in ((bool X) \ ((bool X) /\ X)) \/ X

then B1:
bool X c= ((bool X) \ ((bool X) /\ X)) \/ X
;o in ((bool X) \ ((bool X) /\ X)) \/ X

let o be object ; :: thesis: ( o in bool X implies b_{1} in ((bool X) \ ((bool X) /\ X)) \/ X )

assume B1: o in bool X ; :: thesis: b_{1} in ((bool X) \ ((bool X) /\ X)) \/ X

end;assume B1: o in bool X ; :: thesis: b

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

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 )
;

end;

suppose AS:
card X = 0
; :: thesis: ex Y being set st

( card X c= card Y & X /\ Y = {} )

( 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 = {}

end;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 <> {}

hence
X /\ Y = {}
; :: thesis: verumassume 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;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

suppose AS:
card X = 1
; :: thesis: ex Y being set st

( card X c= card Y & X /\ Y = {} )

( 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 = {}

end;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 <> {}

hence
X /\ Y = {}
; :: thesis: verumassume 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;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

suppose AS:
card X = 2
; :: thesis: ex Y being set st

( card X c= card Y & X /\ Y = {} )

( 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 = {}

end;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 <> {}

hence
X /\ Y = {}
; :: thesis: verumassume 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;

end;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;

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 = {} )

( card X c= card Y & X /\ Y = {} )

reconsider n = card X as Nat by AS;

( card X c= card Y & X /\ Y = {} ) by C; :: thesis: verum

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

B0:
card (bool X) = exp (2,n)
by CARD_2:31;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;then n <= 2 by NAT_1:13;

then not not n = 0 & ... & not n = 2 ;

hence contradiction by AS; :: thesis: verum

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

hence
ex Y being set st 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;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

( card X c= card Y & X /\ Y = {} ) by C; :: thesis: verum

suppose AS:
not card X is finite
; :: thesis: ex Y being set st

( card X c= card Y & X /\ Y = {} )

( card X c= card Y & X /\ Y = {} ) by C; :: thesis: verum

end;

( card X c= card Y & X /\ Y = {} )

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

hence
ex Y being set st 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;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

( card X c= card Y & X /\ Y = {} ) by C; :: thesis: verum