set I = AuxBottom L;
AuxBottom L in Aux L by Def8;
then reconsider I = AuxBottom L as Element of (InclPoset (Aux L)) by YELLOW_1:1;
take I ; :: according to YELLOW_0:def 4 :: thesis: I is_<=_than the carrier of (InclPoset (Aux L))
I is_<=_than the carrier of (InclPoset (Aux L))
proof
let b be Element of (InclPoset (Aux L)); :: according to LATTICE3:def 8 :: thesis: ( not b in the carrier of (InclPoset (Aux L)) or I <= b )
assume b in the carrier of (InclPoset (Aux L)) ; :: thesis: I <= b
then b in Aux L by YELLOW_1:1;
then reconsider b9 = b as auxiliary Relation of L by Def8;
I c= b9 by Th4;
hence I <= b by YELLOW_1:3; :: thesis: verum
end;
hence I is_<=_than the carrier of (InclPoset (Aux L)) ; :: thesis: verum