reconsider A = P, B = Q as Subset of T ;
A1: B is open by PRE_TOPC:def 2;
A is open by PRE_TOPC:def 2;
then P \/ Q is open by A1;
hence P \/ Q is Element of Topology_of T by PRE_TOPC:def 2; :: thesis: verum