definition
let k,l be Nat;
pred k is_factor_of l
means
:FACTOR:
The Nat in let k,l be Nat indicates that the mode of k and l is a natural number. :FACTOR: is a label and this is used for citation later. The labels in the definition are put between the colons. When the abstract file is made by pulling it out of here, it will be changed to def with numbers. Labels of normal theorems will be changed to simple numbers. Also, in k symbolizes multiplication.