let N be complete meet-continuous Lawson TopLattice; :: thesis: ( InclPoset (sigma N) is continuous implies ( N is T_2 iff for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed ) )
assume A1:
InclPoset (sigma N) is continuous
; :: thesis: ( N is T_2 iff for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed )
A2:
[:the carrier of N,the carrier of N:] = the carrier of [:N,N:]
by BORSUK_1:def 5;
hereby :: thesis: ( ( for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed ) implies N is T_2 )
assume A3:
N is
T_2
;
:: thesis: for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed let X be
Subset of
[:N,N:];
:: thesis: ( X = the InternalRel of N implies X is closed )assume A4:
X = the
InternalRel of
N
;
:: thesis: X is closed set INF =
inf_op N;
set f =
<:(pr1 the carrier of N,the carrier of N),(inf_op N):>;
A5:
the
carrier of
[:N,N:] = [:the carrier of N,the carrier of N:]
by YELLOW_3:def 2;
then reconsider f =
<:(pr1 the carrier of N,the carrier of N),(inf_op N):> as
Function of
[:N,N:],
[:N,N:] by A2, FUNCT_3:78;
A6:
for
x,
y being
Element of
N holds
f . [x,y] = [x,(x "/\" y)]
proof
let x,
y be
Element of
N;
:: thesis: f . [x,y] = [x,(x "/\" y)]
A7:
dom (pr1 the carrier of N,the carrier of N) = [:the carrier of N,the carrier of N:]
by FUNCT_2:def 1;
A8:
dom (inf_op N) = [:the carrier of N,the carrier of N:]
by A5, FUNCT_2:def 1;
[x,y] in [:the carrier of N,the carrier of N:]
by ZFMISC_1:106;
hence f . [x,y] =
[((pr1 the carrier of N,the carrier of N) . x,y),((inf_op N) . x,y)]
by A7, A8, FUNCT_3:69
.=
[x,((inf_op N) . x,y)]
by FUNCT_3:def 5
.=
[x,(x "/\" y)]
by WAYBEL_2:def 4
;
:: thesis: verum
end; reconsider D =
id the
carrier of
N as
Subset of
[:N,N:] by BORSUK_1:def 5;
A9:
D is
closed
by A3, YELLOW12:46;
reconsider INF =
inf_op N as
Function of
[:N,N:],
N by A2, A5;
N is
topological_semilattice
by A1, Th22;
then A10:
INF is
continuous
by YELLOW13:def 5;
pr1 the
carrier of
N,the
carrier of
N is
continuous Function of
[:N,N:],
N
by YELLOW12:39;
then A11:
f is
continuous
by A10, YELLOW12:41;
X = f " D
proof
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: f " D c= X
let a be
set ;
:: thesis: ( a in X implies a in f " D )assume A12:
a in X
;
:: thesis: a in f " Dthen consider s,
t being
set such that A13:
(
s in the
carrier of
N &
t in the
carrier of
N &
a = [s,t] )
by A4, ZFMISC_1:def 2;
reconsider s =
s,
t =
t as
Element of
N by A13;
s <= t
by A4, A12, A13, ORDERS_2:def 9;
then
s "/\" t = s
by YELLOW_0:25;
then
f . [s,t] = [s,s]
by A6;
then A14:
f . a in D
by A13, RELAT_1:def 10;
dom f = the
carrier of
[:N,N:]
by FUNCT_2:def 1;
then
a in dom f
by A2, A13, ZFMISC_1:106;
hence
a in f " D
by A14, FUNCT_1:def 13;
:: thesis: verum
end;
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in f " D or a in X )
assume A15:
a in f " D
;
:: thesis: a in X
then A16:
(
a in dom f &
f . a in D )
by FUNCT_1:def 13;
consider s,
t being
set such that A17:
(
s in the
carrier of
N &
t in the
carrier of
N &
a = [s,t] )
by A2, A15, ZFMISC_1:def 2;
reconsider s =
s,
t =
t as
Element of
N by A17;
f . a = [s,(s "/\" t)]
by A6, A17;
then
s = s "/\" t
by A16, RELAT_1:def 10;
then
s <= t
by YELLOW_0:25;
hence
a in X
by A4, A17, ORDERS_2:def 9;
:: thesis: verum
end; hence
X is
closed
by A9, A11, PRE_TOPC:def 12;
:: thesis: verum
end;
assume A18:
for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed
; :: thesis: N is T_2
A19:
id the carrier of N = the InternalRel of N /\ the InternalRel of (N ~ )
for A being Subset of [:N,N:] st A = id the carrier of N holds
A is closed
proof
let A be
Subset of
[:N,N:];
:: thesis: ( A = id the carrier of N implies A is closed )
assume A20:
A = id the
carrier of
N
;
:: thesis: A is closed
reconsider X = the
InternalRel of
N,
Y = the
InternalRel of
(N ~ ) as
Subset of
[:N,N:] by BORSUK_1:def 5;
reconsider X =
X,
Y =
Y as
Subset of
[:N,N:] ;
reconsider f =
<:(pr2 the carrier of N,the carrier of N),(pr1 the carrier of N,the carrier of N):> as
continuous Function of
[:N,N:],
[:N,N:] by YELLOW12:42;
A21:
dom f = [:the carrier of N,the carrier of N:]
by YELLOW12:4;
A22:
X is
closed
by A18;
A23:
f .: X = Y
f is
being_homeomorphism
by YELLOW12:43;
then
Y is
closed
by A22, A23, TOPS_2:72;
hence
A is
closed
by A19, A20, A22, TOPS_1:35;
:: thesis: verum
end;
hence
N is T_2
by YELLOW12:46; :: thesis: verum