まず，predicate の定義について説明します．例えば，k，lを自然数として，いま，kはlの因子である，という定義をしたいとします．これは predicate です．k is factor of l ，このような定義をしたいとします．これは二項演算子の様な形をしてますけれども，k ，l と２つ変数を持っているわけです．この場合どうやって定義を書くかというと，
definition
let k,l be Nat;
pred k is_factor_of l
means
:FACTOR:
ex t being Nat st l=k ・ t;
となります．let k,l be Nat の Nat は，k，l の Mode が自然数であることをあらわしています．:FACTOR: はラベルで，後で引用するときにこのラベルを使います．定義のなかのラベルは両側をコロンではさみます．そして，これは abstract file をここから抜きだして作るときには，def に数字がついたものに変えられます．ふつうの定理のラベルは単なる数字に変えられます．また，k ・ t の ・ はかけ算です．
これで，k is_factor_of l という predicate とは
ex t being Nat st l=k ・ t ということを意味しています．