let T be TopStruct ; :: thesis: ( T is empty implies T is T_0 )
assume A1: T is empty ; :: thesis: T is T_0
let x, y be Point of T; :: according to PRE_TOPC:def 8 :: thesis: ( ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) implies x = y )
assume for G being Subset of T st G is open holds
( x in G iff y in G ) ; :: thesis: x = y
thus x = {} by A1, SUBSET_1:def 1
.= y by A1, SUBSET_1:def 1 ; :: thesis: verum