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

proof

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

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

proof

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

end;

end;

assume for x being Element of X holds f . x <= g . x ; :: thesis: f is_less_than g
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: verum

end;