let X be non empty TopSpace; :: thesis: for A being Subset of X holds the topology of X c= A -extension_of_the_topology_of X
let A be Subset of X; :: thesis: the topology of X c= A -extension_of_the_topology_of X

now :: thesis: for W being object st W in the topology of X holds
W in A -extension_of_the_topology_of X

{} X = {} ;
then reconsider G = {} as Subset of X ;
let W be object ; :: thesis: ( W in the topology of X implies W in A -extension_of_the_topology_of X )
assume A1: W in the topology of X ; :: thesis: W in A -extension_of_the_topology_of X
then reconsider H = W as Subset of X ;
( H = H \/ (G /\ A) & G in the topology of X ) by PRE_TOPC:1;
hence W in A -extension_of_the_topology_of X by A1; :: thesis: verum

end;

hence the topology of X c= A -extension_of_the_topology_of X by TARSKI:def 3; :: thesis: verum