let T be non empty TopSpace; :: thesis: Top (InclPoset the topology of T) = the carrier of T
set L = InclPoset the topology of T;
set C = the carrier of T;
the carrier of T = "/\" ({},(InclPoset the topology of T))

proof

reconsider C = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:def 1;
A1: for b being Element of (InclPoset the topology of T) st b is_<=_than {} holds
C >= b

proof

let b be Element of (InclPoset the topology of T); :: thesis: ( b is_<=_than {} implies C >= b )
assume b is_<=_than {} ; :: thesis: C >= b
b in the topology of T ;
hence C >= b by Th3; :: thesis: verum

end;

C is_<=_than {} ;
hence the carrier of T = "/\" ({},(InclPoset the topology of T)) by A1, YELLOW_0:31; :: thesis: verum

end;

hence Top (InclPoset the topology of T) = the carrier of T by YELLOW_0:def 12; :: thesis: verum