:: deftheorem Def5 defines leq AOFA_I00:def 5 :
for t1, t2, b₃ being INT -valued Function holds
( b₃ = leq (t1,t2) iff ( dom b₃ = (dom t1) /\ (dom t2) & ( for s being object st s in dom b₃ holds
b₃ . s = IFGT ((t1 . s),(t2 . s),0,1) ) ) );