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

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

{} 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;

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: verum