theorem lttrd (G: wff) (a b c: nat): $ G -> a < b $ > $ G -> b < c $ > $ G -> a < c $;
a < b -> b < c -> a < c
G -> a < b
G -> b < c
G -> a < c