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:
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:
thus C /\ D in A -extension_of_the_topology_of X :: thesis: verum
proof
{} X = {} ;
then reconsider H = {} as Subset of X ;
A4: ( C /\ D = H \/ ((C /\ G) /\ A) & H in the topology of X ) by ;
C /\ G in the topology of X by ;
hence C /\ D in A -extension_of_the_topology_of X by A4; :: thesis: verum
end;