let T be non empty TopSpace; :: thesis: not InclPoset the topology of T is trivial
set L = InclPoset the topology of T;
reconsider E = {} , S = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:1, PRE_TOPC:def 1;
E <> S ;
hence not InclPoset the topology of T is trivial by STRUCT_0:def 10; :: thesis: verum