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:58;
A1: Bottom L <= l by YELLOW_0:44;
A2: Bottom S <= s by YELLOW_0:44;
Bottom S >= s by A1, YELLOW_0:60;
hence Bottom S = Bottom L by A2, ORDERS_2:2; :: thesis: verum