set E = Topology_of T;
thus Topology_of T is open :: thesis: Topology_of T is all-open-containing

proof

let A be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not A in Topology_of T or A is open )
assume A in Topology_of T ; :: thesis: A is open
hence A is open by PRE_TOPC:def 5; :: thesis: verum

end;

Topology_of T is all-open-containing

proof

let A be Subset of T; :: according to TOPGEN_4:def 2 :: thesis: ( A is open implies A in Topology_of T )
assume A is open ; :: thesis: A in Topology_of T
hence A in Topology_of T by PRE_TOPC:def 5; :: thesis: verum

end;

hence Topology_of T is all-open-containing ; :: thesis: verum