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 ;
consider x being object such that
x in the carrier of T and
A6: C = Class ((),x) by ;
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 ;
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 ;
then [p,y] in Indiscernibility T by ;
hence p in A by A1, A5, A8, Def3; :: thesis: verum
end;
hence C c= A by TARSKI:def 3; :: thesis: verum