C-4-^==C-hB.o.A = B

[Hp. Pp3 : : A H- C = B -+- C . Pp 2 : : Ts] 2'. A-+-C = B-hC.o.A = B [2^,3]

[Hp. Pp3:o:C-+-A = CH-B.Pp2i:o:Ts]

ffip. Ppl.l, :o:A-hC = B-f-C.B-4-C = B-hD:o:Ts] '4. A = B.A-4-C = B-f-D.o.C = D [1.2J

[Hp. Ppl : : A-f-C=^BH-C . Hp : : BH-C=B-hD . Pp2, : : Ts] 5. C = D.A-4-C = B-f-D..o.A = B * [li.2]

[Hp. Ppli : : A-hC=A-hD . Hp : : A-hD=B-i-D . Pp2 : : Ts]