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