let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for S being with_bottom Subset of L holds subrelstr S is lower-bounded
let S be with_bottom Subset of L; :: thesis: subrelstr S is lower-bounded
Bottom L in S by Def8;
then reconsider dL = Bottom L as Element of (subrelstr S) by YELLOW_0:def 15;
take dL ; :: according to YELLOW_0:def 4 :: thesis: dL is_<=_than the carrier of (subrelstr S)

now :: thesis: for x being Element of (subrelstr S) st x in the carrier of (subrelstr S) holds
dL <= x

let x be Element of (subrelstr S); :: thesis: ( x in the carrier of (subrelstr S) implies dL <= x )
assume x in the carrier of (subrelstr S) ; :: thesis: dL <= x
reconsider x1 = x as Element of L by YELLOW_0:58;
Bottom L <= x1 by YELLOW_0:44;
hence dL <= x by YELLOW_0:60; :: thesis: verum

end;

hence dL is_<=_than the carrier of (subrelstr S) ; :: thesis: verum