let T be 1 -element 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;
A2: {} in the topology of T by PRE_TOPC:1;
A3: the carrier of T in the topology of T by PRE_TOPC:def 1;
A4: bool {x} = {{},{x}} by ZFMISC_1:24;
hence bool the carrier of T c= the topology of T by A1, A2, A3, ZFMISC_1:32; :: 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, A3, A4, ZFMISC_1:32; :: according to XBOOLE_0:def 10 :: thesis: verum