defpred S1[ set , set ] means for A being Subset of T st A is open holds
( $1 in A iff $2 in A );
consider R being Relation of the carrier of T, the carrier of T such that
A1:
for p, q being Element of T holds
( [p,q] in R iff S1[p,q] )
from RELSET_1:sch 2();
A2:
R is_transitive_in the carrier of T
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( not x in the carrier of T or not y in the carrier of T or not z in the carrier of T or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that A3:
(
x in the
carrier of
T &
y in the
carrier of
T &
z in the
carrier of
T )
and A4:
[x,y] in R
and A5:
[y,z] in R
;
[x,z] in R
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
T by A3;
for
A being
Subset of
T st
A is
open holds
(
x9 in A iff
z9 in A )
hence
[x,z] in R
by A1;
verum
end;
R is_reflexive_in the carrier of T
then A8:
( dom R = the carrier of T & field R = the carrier of T )
by ORDERS_1:13;
R is_symmetric_in the carrier of T
then reconsider R = R as Equivalence_Relation of the carrier of T by A8, A2, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
take
R
; for p, q being Point of T holds
( [p,q] in R iff for A being Subset of T st A is open holds
( p in A iff q in A ) )
let p, q be Point of T; ( [p,q] in R iff for A being Subset of T st A is open holds
( p in A iff q in A ) )
thus
( [p,q] in R implies for A being Subset of T st A is open holds
( p in A iff q in A ) )
by A1; ( ( for A being Subset of T st A is open holds
( p in A iff q in A ) ) implies [p,q] in R )
assume
for A being Subset of T st A is open holds
( p in A iff q in A )
; [p,q] in R
hence
[p,q] in R
by A1; verum