let T be non empty TopSpace; :: thesis: InclPoset the topology of T is lower-bounded
set L = InclPoset the topology of T;
reconsider x = {} as Element of (InclPoset the topology of T) by PRE_TOPC:1;

now :: thesis: ex x being Element of (InclPoset the topology of T) st x is_<=_than the carrier of (InclPoset the topology of T)

take x = x; :: thesis: x is_<=_than the carrier of (InclPoset the topology of T)
thus x is_<=_than the carrier of (InclPoset the topology of T) :: thesis: verum

proof

let b be Element of (InclPoset the topology of T); :: according to LATTICE3:def 8 :: thesis: ( not b in the carrier of (InclPoset the topology of T) or x <= b )
assume b in the carrier of (InclPoset the topology of T) ; :: thesis: x <= b
x c= b ;
hence x <= b by Th3; :: thesis: verum

end;

end;

hence InclPoset the topology of T is lower-bounded by YELLOW_0:def 4; :: thesis: verum