Description: A lattice ordering is reflexive. ( ssid analog.) (Contributed by NM, 8-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | latref.b | ||
latref.l | |||
Assertion | latref |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latref.b | ||
2 | latref.l | ||
3 | latpos | ||
4 | 1 2 | posref | |
5 | 3 4 | sylan |