let r, A be Subset of GX; :: thesis: ( ( for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) implies for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G ) )
assume A6: for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
A meets G ) ; :: thesis: for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G )
let p be set ; :: thesis: ( p in the carrier of GX implies ( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G ) )
assume A7: p in the carrier of GX ; :: thesis: ( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G )
thus ( p in r implies for G being Subset of GX st G is open & p in G holds
r meets G ) by XBOOLE_0:3; :: thesis: ( ( for G being Subset of GX st G is open & p in G holds
r meets G ) implies p in r )
assume A8: for G being Subset of GX st G is open & p in G holds
r meets G ; :: thesis: p in r

A9: now :: thesis: for C being Subset of GX st C is closed & A c= C holds
p in C

let C be Subset of GX; :: thesis: ( C is closed & A c= C implies p in C )
assume C is closed ; :: thesis: ( A c= C implies p in C )
then A10: ([#] GX) \ C is open ;

now :: thesis: ( p in ([#] GX) \ C implies A meets ([#] GX) \ C )

assume p in ([#] GX) \ C ; :: thesis: A meets ([#] GX) \ C
then r meets ([#] GX) \ C by A8, A10;
then ex x being object st
( x in r & x in ([#] GX) \ C ) by XBOOLE_0:3;
hence A meets ([#] GX) \ C by A6, A10; :: thesis: verum

end;

then ( not A c= (([#] GX) \ C) ` or p in C or not p in [#] GX ) by SUBSET_1:23, XBOOLE_0:def 5;
hence ( A c= C implies p in C ) by A7, Th3; :: thesis: verum

end;

for G being Subset of GX st G is open & p in G holds
A meets G

proof

let G be Subset of GX; :: thesis: ( G is open & p in G implies A meets G )
assume A11: G is open ; :: thesis: ( not p in G or A meets G )
([#] GX) \ (([#] GX) \ G) = G by Th3;
then ([#] GX) \ G is closed by A11;
then ( A c= G ` implies p in ([#] GX) \ G ) by A9;
hence ( not p in G or A meets G ) by SUBSET_1:23, XBOOLE_0:def 5; :: thesis: verum

end;

hence p in r by A6, A7; :: thesis: verum