Metamath Proof Explorer

Theorem weso

Description: A well-ordering is a strict ordering. (Contributed by NM, 16-Mar-1997)

Ref Expression
Assertion weso 
|- ( R We A -> R Or A )

Proof

Step Hyp Ref Expression
1 df-we 
 |-  ( R We A <-> ( R Fr A /\ R Or A ) )
2 1 simprbi 
 |-  ( R We A -> R Or A )