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