let S be full SubRelStr of L; :: thesis: ( S is bottom-inheriting implies ( not S is empty & S is lower-bounded ) )
assume A1: Bottom L in the carrier of S ; :: according to WAYBEL34:def 19 :: thesis: ( not S is empty & S is lower-bounded )
hence A2: not S is empty ; :: thesis: S is lower-bounded
reconsider x = Bottom L as Element of S by A1;
take x ; :: according to YELLOW_0:def 4 :: thesis: x is_<=_than the carrier of S
let y be Element of S; :: according to LATTICE3:def 8 :: thesis: ( not y in the carrier of S or x <= y )
assume A3: y in the carrier of S ; :: thesis: x <= y
reconsider a = y as Element of L by A2, YELLOW_0:58;
Bottom L <= a by YELLOW_0:44;
hence x <= y by A3, YELLOW_0:60; :: thesis: verum