let P be Subset of S; :: according to TOPS_2:def 1 :: thesis: ( not P in the topology of S or P is open )

thus ( not P in the topology of S or P is open ) ; :: thesis: verum

thus ( not P in the topology of S or P is open ) ; :: thesis: verum