let L be lower-bounded sup-Semilattice; :: thesis: Top (InclPoset (Aux L)) = IntRel L
IntRel L = "/\" ({},(InclPoset (Aux L)))

proof

set P = InclPoset (Aux L);
set I = IntRel L;
IntRel L in Aux L by Def8;
then reconsider I = IntRel L as Element of (InclPoset (Aux L)) by YELLOW_1:1;
A1: I is_<=_than {} ;
for b being Element of (InclPoset (Aux L)) st b is_<=_than {} holds
I >= b

proof

let b be Element of (InclPoset (Aux L)); :: thesis: ( b is_<=_than {} implies I >= 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;
assume b is_<=_than {} ; :: thesis: I >= b
b9 c= I by Th2;
hence I >= b by YELLOW_1:3; :: thesis: verum

end;

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

end;

hence Top (InclPoset (Aux L)) = IntRel L ; :: thesis: verum