Description: 'Less than or equal to' is reflexive. (Contributed by NM, 18Aug1999)
Ref  Expression  

Assertion  leid   ( A e. RR > A <_ A ) 
Step  Hyp  Ref  Expression 

1  eqid   A = A 

2  1  olci   ( A < A \/ A = A ) 
3  leloe   ( ( A e. RR /\ A e. RR ) > ( A <_ A <> ( A < A \/ A = A ) ) ) 

4  2 3  mpbiri   ( ( A e. RR /\ A e. RR ) > A <_ A ) 
5  4  anidms   ( A e. RR > A <_ A ) 