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 x' = x as Element of L ;
A2: R1 -below x' c= R2 -below x'

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in R1 -below x' or a in R2 -below x' )
assume a in R1 -below x' ; :: thesis: a in R2 -below x'
then consider b being Element of L such that
A3: ( b = a & [b,x'] in R1 ) ;
thus a in R2 -below x' by A1, A3; :: thesis: verum

end;

reconsider A1 = (R1 -below ) . x', A2 = (R2 -below ) . x' 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 )
( (R1 -below ) . x = R1 -below x' & (R2 -below ) . x = R2 -below x' ) by Def13;
hence ( A1 = (R1 -below ) . x & A2 = (R2 -below ) . x & A1 <= A2 ) by A2, YELLOW_1:3; :: thesis: verum