let T be non empty trivial TopSpace; :: thesis: ( the topology of T = bool the carrier of T & ( for x being Point of T holds
( the carrier of T = {x} & the topology of T = {{} ,{x}} ) ) )
thus the topology of T c= bool the carrier of T ; :: according to XBOOLE_0:def 10 :: thesis: ( bool the carrier of T c= the topology of T & ( for x being Point of T holds
( the carrier of T = {x} & the topology of T = {{} ,{x}} ) ) )
consider x being Point of T such that
A1: the carrier of T = {x} by TEX_1:def 1;
( {} in the topology of T & the carrier of T in the topology of T ) by PRE_TOPC:5, PRE_TOPC:def 1;
then A2: ( {{} ,the carrier of T} c= the topology of T & bool {x} = {{} ,{x}} ) by ZFMISC_1:30, ZFMISC_1:38;
hence bool the carrier of T c= the topology of T by A1; :: thesis: for x being Point of T holds
( the carrier of T = {x} & the topology of T = {{} ,{x}} )
let a be Point of T; :: thesis: ( the carrier of T = {a} & the topology of T = {{} ,{a}} )
a = x by STRUCT_0:def 10;
hence ( the carrier of T = {a} & the topology of T c= {{} ,{a}} & {{} ,{a}} c= the topology of T ) by A1, A2; :: according to XBOOLE_0:def 10 :: thesis: verum