Theorem 3oalem4

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	3oalem4.3	|- R = ( ( _|_ ` B ) i^i ( B vH A ) )
Assertion	3oalem4	|- R C_ ( _|_ ` B )

Proof

Step	Hyp	Ref	Expression
1		3oalem4.3	|- R = ( ( _|_ ` B ) i^i ( B vH A ) )
2		inss1	|- ( ( _|_ ` B ) i^i ( B vH A ) ) C_ ( _|_ ` B )
3	1 2	eqsstri	|- R C_ ( _|_ ` B )