let L be lower-bounded with_suprema Poset; :: thesis: Bottom (InclPoset (Aux L)) = AuxBottom L
AuxBottom L in Aux L by Def8;
then reconsider N = AuxBottom L as Element of (InclPoset (Aux L)) by YELLOW_1:1;
A1: N is_>=_than {} ;
for b being Element of (InclPoset (Aux L)) st b is_>=_than {} holds
N <= b

proof

let b be Element of (InclPoset (Aux L)); :: thesis: ( b is_>=_than {} implies N <= b )
assume b is_>=_than {} ; :: thesis: N <= b
b in the carrier of (InclPoset (Aux L)) ;
then b in Aux L by YELLOW_1:1;
then reconsider b9 = b as auxiliary Relation of L by Def8;
N c= b9 by Th4;
hence N <= b by YELLOW_1:3; :: thesis: verum

end;

hence Bottom (InclPoset (Aux L)) = AuxBottom L by A1, YELLOW_0:30; :: thesis: verum