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 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 full 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 full 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 A1: ( f' = f & g' = g & 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 S st
( b₁ = f . x & b₂ = g . x & b₁ <= b₂ ) )
assume A2: 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:7;
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 a', b' being Element of L st
( a' = a & b' = b & a' <= b' ) by A1, A2, YELLOW_2:def 1;
hence a <= b by YELLOW_0:61; :: thesis: verum