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;
take I ; :: according to YELLOW_0:def 5 :: thesis: the carrier of (InclPoset (Aux L)) is_<=_than I
I is_>=_than the carrier of (InclPoset (Aux L))

proof

let b be Element of (InclPoset (Aux L)); :: according to LATTICE3:def 9 :: thesis: ( not b in the carrier of (InclPoset (Aux L)) or b <= I )
assume b in the carrier of (InclPoset (Aux L)) ; :: thesis: b <= I
then b in Aux L by YELLOW_1:1;
then reconsider b9 = b as auxiliary Relation of L by Def8;
b9 c= I by Th2;
hence b <= I by YELLOW_1:3; :: thesis: verum

end;

hence the carrier of (InclPoset (Aux L)) is_<=_than I ; :: thesis: verum