let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for S being non empty full bottom-inheriting SubRelStr of L holds Bottom S = Bottom L
let S be non empty full bottom-inheriting SubRelStr of L; :: thesis: Bottom S = Bottom L
reconsider s = Bottom L as Element of S by Def19;
reconsider l = Bottom S as Element of L by YELLOW_0:59;
Bottom L <= l by YELLOW_0:44;
then ( Bottom S <= s & Bottom S >= s ) by YELLOW_0:44, YELLOW_0:61;
hence Bottom S = Bottom L by ORDERS_2:25; :: thesis: verum