take {} T ; :: thesis: {} T is open
thus {} T in the topology of T by Th5; :: according to PRE_TOPC:def 5 :: thesis: verum