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 x' = x as Element of L ;
A1: (AR -below ) . x' = AR -below x' by Def13;
(IdsMap L) . x' = downarrow x' by YELLOW_2:def 4;
then A2: (AR -below ) . x c= (IdsMap L) . x by A1, Th12;
reconsider a = (AR -below ) . x', b = (IdsMap L) . x' 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