let X be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( f9 = f & g9 = g & f9 <= g9 implies f <= g )
assume that
A1: f9 = f and
A2: g9 = g and
A3: f9 <= g9 ; :: thesis: f <= g
let x be set ; :: according to YELLOW_2:def 1 :: thesis: ( not x in X or ex b₁, b₂ being Element of the carrier of S st
( b₁ = f . x & b₂ = g . x & b₁ <= b₂ ) )
assume A4: x in X ; :: thesis: ex b₁, b₂ being Element of the carrier of S st
( b₁ = f . x & b₂ = g . x & b₁ <= b₂ )
then reconsider a = f . x, b = g . x as Element of S by FUNCT_2:5;
take a ; :: thesis: ex b₁ being Element of the carrier of S st
( a = f . x & b₁ = g . x & a <= b₁ )
take b ; :: thesis: ( a = f . x & b = g . x & a <= b )
thus ( a = f . x & b = g . x ) ; :: thesis: 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; :: thesis: verum