let L be lower-bounded sup-Semilattice; :: thesis: for R1, R2 being auxiliary Relation of L st R1 c= R2 holds
R1 -below <= R2 -below
let R1, R2 be auxiliary Relation of L; :: thesis: ( R1 c= R2 implies R1 -below <= R2 -below )
assume A1: R1 c= R2 ; :: thesis: R1 -below <= R2 -below
let x be set ; :: according to YELLOW_2:def 1 :: thesis: ( not x in the carrier of L or ex b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) st
( b₁ = (R1 -below) . x & b₂ = (R2 -below) . x & b₁ <= b₂ ) )
assume x in the carrier of L ; :: thesis: ex b₁, b₂ being Element of the carrier of (InclPoset (Ids L)) st
( b₁ = (R1 -below) . x & b₂ = (R2 -below) . x & b₁ <= b₂ )
then reconsider x9 = x as Element of L ;
A2: R1 -below x9 c= R2 -below x9

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in R1 -below x9 or a in R2 -below x9 )
assume a in R1 -below x9 ; :: thesis: a in R2 -below x9
then ex b being Element of L st
( b = a & [b,x9] in R1 ) ;
hence a in R2 -below x9 by A1; :: thesis: verum

end;

reconsider A1 = (R1 -below) . x9, A2 = (R2 -below) . x9 as Element of (InclPoset (Ids L)) ;
take A1 ; :: thesis: ex b₁ being Element of the carrier of (InclPoset (Ids L)) st
( A1 = (R1 -below) . x & b₁ = (R2 -below) . x & A1 <= b₁ )
take A2 ; :: thesis: ( A1 = (R1 -below) . x & A2 = (R2 -below) . x & A1 <= A2 )
A3: (R1 -below) . x = R1 -below x9 by Def12;
(R2 -below) . x = R2 -below x9 by Def12;
hence ( A1 = (R1 -below) . x & A2 = (R2 -below) . x & A1 <= A2 ) by A2, A3, YELLOW_1:3; :: thesis: verum