let L, M be non empty RelStr ; :: thesis: for f, g being Function of L,M holds
( f <= g iff for x being Element of L holds f . x <= g . x )
let f, g be Function of L,M; :: thesis: ( f <= g iff for x being Element of L holds f . x <= g . x )

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

assume A1: f <= g ; :: thesis: for x being Element of L holds f . x <= g . x
let x be Element of L; :: thesis: f . x <= g . x
ex m1, m2 being Element of M st
( m1 = f . x & m2 = g . x & m1 <= m2 ) by A1;
hence f . x <= g . x ; :: thesis: verum

end;

assume A2: for x being Element of L holds f . x <= g . x ; :: thesis: f <= g
let x be set ; :: according to YELLOW_2:def 1 :: thesis: ( x in the carrier of L implies ex a, b being Element of M st
( a = f . x & b = g . x & a <= b ) )
assume x in the carrier of L ; :: thesis: ex a, b being Element of M st
( a = f . x & b = g . x & a <= b )
then reconsider x = x as Element of L ;
take f . x ; :: thesis: ex b being Element of M st
( f . x = f . x & b = g . x & f . x <= b )
take g . x ; :: thesis: ( f . x = f . x & g . x = g . x & f . x <= g . x )
thus ( f . x = f . x & g . x = g . x & f . x <= g . x ) by A2; :: thesis: verum