let T be non empty T_0 TopSpace; :: thesis: for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds
card the carrier of T c= card the carrier of L1
let L1 be continuous sup-Semilattice; :: thesis: ( InclPoset the topology of T = L1 implies card the carrier of T c= card the carrier of L1 )
A1: card the carrier of T c= card the topology of T by YELLOW15:28;
assume InclPoset the topology of T = L1 ; :: thesis: card the carrier of T c= card the carrier of L1
hence card the carrier of T c= card the carrier of L1 by A1, YELLOW_1:1; :: thesis: verum