take T ; :: thesis: ( [#] T c= [#] T & ( for P being Subset of T holds
( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) ) ) )
thus [#] T c= [#] T ; :: thesis: for P being Subset of T holds
( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) )
let P be Subset of T; :: thesis: ( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) )
hereby :: thesis: ( ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) implies P in the topology of T )
assume A1: P in the topology of T ; :: thesis: ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) )
take Q = P; :: thesis: ( Q in the topology of T & P = Q /\ ([#] T) )
thus Q in the topology of T by A1; :: thesis: P = Q /\ ([#] T)
thus P = Q /\ ([#] T) by XBOOLE_1:28; :: thesis: verum
end;
given Q being Subset of T such that A2: ( Q in the topology of T & P = Q /\ ([#] T) ) ; :: thesis: P in the topology of T
thus P in the topology of T by A2, XBOOLE_1:28; :: thesis: verum