let X be set ; :: thesis: for L being non empty RelStr
for S being non empty 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 & f <= g holds
f9 <= g9
let L be non empty RelStr ; :: thesis: for S being non empty 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 & f <= g holds
f9 <= g9
let S be non empty 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 & f <= g holds
f9 <= g9
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 & f <= g holds
f9 <= g9
let f9, g9 be Function of X, the carrier of L; :: thesis: ( f9 = f & g9 = g & f <= g implies f9 <= g9 )
assume that
A1: f9 = f and
A2: g9 = g and
A3: f <= g ; :: thesis: f9 <= g9
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 L st
( b₁ = f9 . x & b₂ = g9 . x & b₁ <= b₂ ) )
assume A4: x in X ; :: thesis: ex b₁, b₂ being Element of the carrier of L st
( b₁ = f9 . x & b₂ = g9 . x & b₁ <= b₂ )
then reconsider a = f . x, b = g . x as Element of S by FUNCT_2:5;
reconsider a9 = a, b9 = b as Element of L by YELLOW_0:58;
take a9 ; :: thesis: ex b₁ being Element of the carrier of L st
( a9 = f9 . x & b₁ = g9 . x & a9 <= b₁ )
take b9 ; :: thesis: ( a9 = f9 . x & b9 = g9 . x & a9 <= b9 )
thus ( a9 = f9 . x & b9 = g9 . x ) by A1, A2; :: thesis: a9 <= b9
ex a, b being Element of S st
( a = f . x & b = g . x & a <= b ) by A3, A4;
hence a9 <= b9 by YELLOW_0:59; :: thesis: verum