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

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

hence
the topology of X c= A -extension_of_the_topology_of X
by TARSKI:def 3; :: thesis: verumW 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;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