let L be lower-bounded with_suprema Poset; :: thesis: Bottom (InclPoset (Aux L)) = AuxBottom L
AuxBottom L in Aux L by Def9;
then reconsider N = AuxBottom L as Element of (InclPoset (Aux L)) by YELLOW_1:1;
AuxBottom L = "\/" {} ,(InclPoset (Aux L))

proof

A1: N is_>=_than {} by YELLOW_0:6;
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 b' = b as auxiliary Relation of L by Def9;
N c= b' by Th4;
hence N <= b by YELLOW_1:3; :: thesis: verum

end;

hence AuxBottom L = "\/" {} ,(InclPoset (Aux L)) by A1, YELLOW_0:30; :: thesis: verum

end;

hence Bottom (InclPoset (Aux L)) = AuxBottom L ; :: thesis: verum