let X be set ; for L being non empty RelStr
for S being non empty full SubRelStr of L
for f, g being Function of X, the carrier of S
for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds
f <= g
let L be non empty RelStr ; for S being non empty full SubRelStr of L
for f, g being Function of X, the carrier of S
for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds
f <= g
let S be non empty full SubRelStr of L; for f, g being Function of X, the carrier of S
for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds
f <= g
let f, g be Function of X, the carrier of S; for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds
f <= g
let f9, g9 be Function of X, the carrier of L; ( f9 = f & g9 = g & f9 <= g9 implies f <= g )
assume that
A1:
f9 = f
and
A2:
g9 = g
and
A3:
f9 <= g9
; f <= g
let x be set ; YELLOW_2:def 1 ( not x in X or ex b1, b2 being Element of the carrier of S st
( b1 = f . x & b2 = g . x & b1 <= b2 ) )
assume A4:
x in X
; ex b1, b2 being Element of the carrier of S st
( b1 = f . x & b2 = g . x & b1 <= b2 )
then reconsider a = f . x, b = g . x as Element of S by FUNCT_2:5;
take
a
; ex b1 being Element of the carrier of S st
( a = f . x & b1 = g . x & a <= b1 )
take
b
; ( a = f . x & b = g . x & a <= b )
thus
( a = f . x & b = g . x )
; a <= b
ex a9, b9 being Element of L st
( a9 = a & b9 = b & a9 <= b9 )
by A1, A2, A3, A4;
hence
a <= b
by YELLOW_0:60; verum