let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary Relation of L holds AR -below <= IdsMap L
let AR be auxiliary Relation of L; :: thesis: AR -below <= IdsMap L
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₁ = (AR -below) . x & b₂ = (IdsMap L) . 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₁ = (AR -below) . x & b₂ = (IdsMap L) . x & b₁ <= b₂ )
then reconsider x9 = x as Element of L ;
A1: (AR -below) . x9 = AR -below x9 by Def12;
(IdsMap L) . x9 = downarrow x9 by YELLOW_2:def 4;
then A2: (AR -below) . x c= (IdsMap L) . x by A1, Th12;
reconsider a = (AR -below) . x9, b = (IdsMap L) . x9 as Element of (InclPoset (Ids L)) ;
take a ; :: thesis: ex b₁ being Element of the carrier of (InclPoset (Ids L)) st
( a = (AR -below) . x & b₁ = (IdsMap L) . x & a <= b₁ )
take b ; :: thesis: ( a = (AR -below) . x & b = (IdsMap L) . x & a <= b )
thus ( a = (AR -below) . x & b = (IdsMap L) . x & a <= b ) by A2, YELLOW_1:3; :: thesis: verum