Theorem tospos

Description: A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018)

	Ref	Expression
Assertion	tospos	$$⊢F\in \mathrm{Toset}\to F\in \mathrm{Poset}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
2		eqid	$$⊢{\le }_F={\le }_F$$
3	1 2	istos	$$⊢F\in \mathrm{Toset}\leftrightarrow \left(F\in \mathrm{Poset}\wedge \forall x\in {\mathrm{Base}}_F\forall y\in {\mathrm{Base}}_F\left(x{\le }_{F}y\vee y{\le }_{F}x\right)\right)$$
4	3	simplbi	$$⊢F\in \mathrm{Toset}\to F\in \mathrm{Poset}$$