Theorem bnj1364

Description: Property of _FrSe . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj1364	⊢ ( 𝑅 FrSe 𝐴 → 𝑅 Se 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-bnj15	⊢ ( 𝑅 FrSe 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) )
2	1	simprbi	⊢ ( 𝑅 FrSe 𝐴 → 𝑅 Se 𝐴 )