let X be non empty TopSpace; :: thesis: for A, C, D being Subset of X st C in the topology of X & D in { (G /\ A) where G is Subset of X : G in the topology of X } holds

( C \/ D in A -extension_of_the_topology_of X & C /\ D in A -extension_of_the_topology_of X )

let A be Subset of X; :: thesis: for C, D being Subset of X st C in the topology of X & D in { (G /\ A) where G is Subset of X : G in the topology of X } holds

( C \/ D in A -extension_of_the_topology_of X & C /\ D in A -extension_of_the_topology_of X )

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

assume A1: C in the topology of X ; :: thesis: ( not D in { (G /\ A) where G is Subset of X : G in the topology of X } or ( C \/ D in A -extension_of_the_topology_of X & C /\ D in A -extension_of_the_topology_of X ) )

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

then consider G being Subset of X such that

A2: D = G /\ A and

A3: G in the topology of X ;

thus C \/ D in A -extension_of_the_topology_of X by A1, A2, A3; :: thesis: C /\ D in A -extension_of_the_topology_of X

thus C /\ D in A -extension_of_the_topology_of X :: thesis: verum

( C \/ D in A -extension_of_the_topology_of X & C /\ D in A -extension_of_the_topology_of X )

let A be Subset of X; :: thesis: for C, D being Subset of X st C in the topology of X & D in { (G /\ A) where G is Subset of X : G in the topology of X } holds

( C \/ D in A -extension_of_the_topology_of X & C /\ D in A -extension_of_the_topology_of X )

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

assume A1: C in the topology of X ; :: thesis: ( not D in { (G /\ A) where G is Subset of X : G in the topology of X } or ( C \/ D in A -extension_of_the_topology_of X & C /\ D in A -extension_of_the_topology_of X ) )

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

then consider G being Subset of X such that

A2: D = G /\ A and

A3: G in the topology of X ;

thus C \/ D in A -extension_of_the_topology_of X by A1, A2, A3; :: thesis: C /\ D in A -extension_of_the_topology_of X

thus C /\ D in A -extension_of_the_topology_of X :: thesis: verum