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

proof

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

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

proof

let x be Element of X; :: thesis: for y being Element of Y holds f . x,y <= g . x,y
let y be Element of Y; :: thesis: f . x,y <= g . x,y
( dom f = [:X,Y:] & [x,y] in [:X,Y:] ) by FUNCT_2:def 1;
hence f . x,y <= g . x,y by A1, FUZZY_1:def 2; :: thesis: verum

end;

end;

assume A2: for x being Element of X
for y being Element of Y holds f . x,y <= g . x,y ; :: thesis: f is_less_than g
A3: for c being set st c in dom f holds
f . c <= g . c

proof

let c be set ; :: thesis: ( c in dom f implies f . c <= g . c )
assume A4: c in dom f ; :: thesis: f . c <= g . c
then consider x, y being set such that
A5: [x,y] = c by RELAT_1:def 1;
reconsider y = y as Element of Y by A4, A5, ZFMISC_1:106;
reconsider x = x as Element of X by A4, A5, ZFMISC_1:106;
f . x,y <= g . x,y by A2;
hence f . c <= g . c by A5; :: thesis: verum

end;

dom g = [:X,Y:] by FUNCT_2:def 1;
hence f is_less_than g by A3, FUZZY_1:def 2; :: thesis: verum

end;