Metamath Proof Explorer


Theorem trclfvlb3

Description: The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020)

Ref Expression
Assertion trclfvlb3 R V R R R t+ R

Proof

Step Hyp Ref Expression
1 trclfvlb R V R t+ R
2 trclfvlb2 R V R R t+ R
3 1 2 unssd R V R R R t+ R