$( <MM> <PROOF ASST> THEOREM=
19.21adv
LOC_AFTER= 19.21adv
* Deduction from Theorem 19.21 of [Margaris] p. 90.
h1::19.21adv.1
2::ax-17
3::ax-17
qed:2,3,1:19.21ad
$= wph wps wch vx wph vx ax-17 wps vx ax-17 19.21adv.1 19.21ad $.
$d
$d
$)