let P be non empty lower-bounded Poset; :: thesis: for p being Element of P st p is_<=_than the carrier of P holds
p = Bottom P
let p be Element of P; :: thesis: ( p is_<=_than the carrier of P implies p = Bottom P )
assume A1: p is_<=_than the carrier of P ; :: thesis: p = Bottom P
A2: ex_sup_of {} ,P by YELLOW_0:42;
A3: {} is_<=_than p ;
for a being Element of P st {} is_<=_than a holds
p <= a by A1;
hence p = Bottom P by A2, A3, YELLOW_0:def 9; :: thesis: verum