0
in
NAT
;
then
{
0
}
c=
NAT
by
TARSKI:def 1
;
then
NAT
/\
(
bool
NAT
)
<>
{}
by
CARD_1:49
,
XBOOLE_0:def 4
;
hence
NAT
meets
bool
NAT
by
XBOOLE_0:def 7
;
:: thesis:
verum