let T be non empty TopSpace; :: thesis: for A being Subset of T st A is open holds
for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A
let A be Subset of T; :: thesis: ( A is open implies for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A )
assume A1: A is open ; :: thesis: for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A
set R = Indiscernibility T;
let C be Subset of T; :: thesis: ( C in Indiscernible T & C meets A implies C c= A )
assume that
A2: C in Indiscernible T and
A3: C meets A ; :: thesis: C c= A
consider y being object such that
A4: y in C and
A5: y in A by A3, XBOOLE_0:3;
consider x being object such that
x in the carrier of T and
A6: C = Class ((Indiscernibility T),x) by A2, EQREL_1:def 3;
for p being object st p in C holds
p in A

proof

let p be object ; :: thesis: ( p in C implies p in A )
[y,x] in Indiscernibility T by A6, A4, EQREL_1:19;
then A7: [x,y] in Indiscernibility T by EQREL_1:6;
assume A8: p in C ; :: thesis: p in A
then [p,x] in Indiscernibility T by A6, EQREL_1:19;
then [p,y] in Indiscernibility T by A7, EQREL_1:7;
hence p in A by A1, A5, A8, Def3; :: thesis: verum

end;

hence C c= A by TARSKI:def 3; :: thesis: verum