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

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

hence
C c= A
by TARSKI:def 3; :: thesis: verum
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;[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