[Q] is an archemaedian ordered field.
*)
-inline procedural "cic:/CoRN/model/ordfields/Qordfield/Qlt_is_strict_order.con".
+inline procedural "cic:/CoRN/model/ordfields/Qordfield/Qlt_is_strict_order.con" as definition.
-inline procedural "cic:/CoRN/model/ordfields/Qordfield/Q_is_COrdField.con".
+inline procedural "cic:/CoRN/model/ordfields/Qordfield/Q_is_COrdField.con" as definition.
-inline procedural "cic:/CoRN/model/ordfields/Qordfield/Q_as_COrdField.con".
+inline procedural "cic:/CoRN/model/ordfields/Qordfield/Q_as_COrdField.con" as definition.
-inline procedural "cic:/CoRN/model/ordfields/Qordfield/Q_is_archemaedian.con".
+inline procedural "cic:/CoRN/model/ordfields/Qordfield/Q_is_archemaedian.con" as theorem.