let S be TopStruct ; :: thesis: the topology of S is open
let P be Subset of S; :: according to TOPS_2:def 1 :: thesis: ( not P in the topology of S or P is open )
assume P in the topology of S ; :: thesis: P is open
hence P is open by PRE_TOPC:def 5; :: thesis: verum