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