let X be non empty TopSpace; :: thesis: for A being Subset of X holds { (G /\ A) where G is Subset of X : G in the topology of X } c= A -extension_of_the_topology_of X

let A be Subset of X; :: thesis: { (G /\ A) where G is Subset of X : G in the topology of X } c= A -extension_of_the_topology_of X

let A be Subset of X; :: thesis: { (G /\ A) where G is Subset of X : G in the topology of X } c= A -extension_of_the_topology_of X

now :: thesis: for W being object st W in { (G /\ A) where G is Subset of X : G in the topology of X } holds

W in A -extension_of_the_topology_of X

hence
{ (G /\ A) where G is Subset of X : G in 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 H = {} as Subset of X ;

let W be object ; :: thesis: ( W in { (G /\ A) where G is Subset of X : G in the topology of X } implies W in A -extension_of_the_topology_of X )

assume W in { (G /\ A) where G is Subset of X : G in the topology of X } ; :: thesis: W in A -extension_of_the_topology_of X

then consider G being Subset of X such that

A1: ( W = G /\ A & G in the topology of X ) ;

( G /\ A = H \/ (G /\ A) & H 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 H = {} as Subset of X ;

let W be object ; :: thesis: ( W in { (G /\ A) where G is Subset of X : G in the topology of X } implies W in A -extension_of_the_topology_of X )

assume W in { (G /\ A) where G is Subset of X : G in the topology of X } ; :: thesis: W in A -extension_of_the_topology_of X

then consider G being Subset of X such that

A1: ( W = G /\ A & G in the topology of X ) ;

( G /\ A = H \/ (G /\ A) & H in the topology of X ) by PRE_TOPC:1;

hence W in A -extension_of_the_topology_of X by A1; :: thesis: verum