Description: Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltltncvr.b | ||
ltltncvr.s | |||
ltltncvr.c | |||
Assertion | ltcvrntr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltltncvr.b | ||
2 | ltltncvr.s | ||
3 | ltltncvr.c | ||
4 | 1 2 3 | cvrlt | |
5 | 4 | ex | |
6 | 5 | 3adant3r1 | |
7 | 1 2 3 | ltltncvr | |
8 | 6 7 | sylan2d |