the carrier of T in the topology of T by Def1;
hence ([#] T) \ ({} T) is open by Def5; :: according to PRE_TOPC:def 6 :: thesis: verum