Next: LIST Up: The Rules Previous: INT

LESS

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* formation

.H >> ext a<b by intro less * H >> int ext a * H >> int ext b . H >> a<b in by intro * H >> a in int * H >> b in int rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex * equality . H >> axiom in a<b * H >> a<b

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995