let A be set ; :: thesis: {} ,A, {} are_mutually_disjoint
a1: {} /\ A = {} ;
{} /\ {} = {} ;
hence {} ,A, {} are_mutually_disjoint by a1, XBOOLE_0:def 7; :: thesis: verum