(a \ ((A \/ a) \ B)) \+\ (a /\ B) = {} ;
hence (a \ (A \ B)) \+\ (a /\ B) is empty ; :: thesis: verum