set p = <*> (bool X);
take <*> (bool X) ; :: thesis: ( not <*> (bool X) is exhaustive & <*> (bool X) is disjoint_valued )
thus not <*> (bool X) is exhaustive :: thesis: <*> (bool X) is disjoint_valued

proof

assume A2: <*> (bool X) is exhaustive ; :: thesis: contradiction
not X is empty ;
then consider a being object such that
A3: a in X ;
consider b being object such that
A4: ( b in dom (<*> (bool X)) & a in (<*> (bool X)) . b ) by A2, A3;
thus contradiction by A4; :: thesis: verum

end;

thus <*> (bool X) is disjoint_valued ; :: thesis: verum