let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for x being Element of L holds Bottom L <= x
let x be Element of L; :: thesis: Bottom L <= x
( {} is_<=_than x & ex_sup_of {} ,L ) by Th42;
hence Bottom L <= x by Th30; :: thesis: verum