thus ( f is_less_than g iff for x being Element of X holds f . x <= g . x ) :: thesis:

proof

hereby :: thesis:

assume A1: f is_less_than g ; :: thesis:
thus for x being Element of X holds f . x <= g . x :: thesis:

proof

let x be Element of X; :: thesis:
dom f = X by FUNCT_2:def 1;
hence f . x <= g . x by A1; :: thesis:

end;

end;

assume for x being Element of X holds f . x <= g . x ; :: thesis:
then ( dom g = X & ( for x being set st x in dom f holds
f . x <= g . x ) ) by FUNCT_2:def 1;
hence f is_less_than g ; :: thesis:

end;