Theorem 3oalem4

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

	Ref	Expression
Hypothesis	3oalem4.3	⊢ 𝑅 = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) )
Assertion	3oalem4	⊢ 𝑅 ⊆ ( ⊥ ‘ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		3oalem4.3	⊢ 𝑅 = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) )
2		inss1	⊢ ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) ⊆ ( ⊥ ‘ 𝐵 )
3	1 2	eqsstri	⊢ 𝑅 ⊆ ( ⊥ ‘ 𝐵 )