Def i z j == j < z i

Thm* i,j:. i z j

Def i < z j == if i < j true ; false fi

Thm* i,j:. i < z j

Def b == if b false else true fi

Thm* b:. b