Description: Part of proof of Lemma E in Crawley p. 113. Value of F at an atom
not under W . TODO: FIX COMMENT. TODO: consolidate uses of
lhpmat here and elsewhere, and presence/absence of
s .<_ ( P .\/ Q ) term. Also, why can proof be shortened with
cdleme27cl ? What is difference from cdlemefs27cl ? (Contributed by NM, 29-Mar-2013)(New usage is discouraged.)