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=\perp \left(B\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
Assertion	3oalem4	$$⊢R\subseteq \perp \left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		3oalem4.3	$$⊢R=\perp \left(B\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
2		inss1	$$⊢\perp \left(B\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)\subseteq \perp \left(B\right)$$
3	1 2	eqsstri	$$⊢R\subseteq \perp \left(B\right)$$