A ^ B is LeftLinearCombination of P \/ P ;
hence A ^ B is LeftLinearCombination of P ; :: thesis: verum