let N be complete Lawson meet-continuous TopLattice; :: thesis: ( InclPoset (sigma N) is continuous implies ( N is Hausdorff 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 Hausdorff 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 2;

X is closed ; :: thesis: N is Hausdorff

A22: the InternalRel of N /\ the InternalRel of (N ~) c= id the carrier of N by YELLOW12:23;

id the carrier of N c= the InternalRel of N /\ the InternalRel of (N ~) by YELLOW12:22;

then A23: id the carrier of N = the InternalRel of N /\ the InternalRel of (N ~) by A22;

for A being Subset of [:N,N:] st A = id the carrier of N holds

A is closed

X is closed ) )

assume A1: InclPoset (sigma N) is continuous ; :: thesis: ( N is Hausdorff 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 2;

hereby :: thesis: ( ( for X being Subset of [:N,N:] st X = the InternalRel of N holds

X is closed ) implies N is Hausdorff )

assume A21:
for X being Subset of [:N,N:] st X = the InternalRel of N holds X is closed ) implies N is Hausdorff )

reconsider D = id the carrier of N as Subset of [:N,N:] by BORSUK_1:def 2;

set INF = inf_op N;

set f = <:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):>;

assume N is Hausdorff ; :: thesis: for X being Subset of [:N,N:] st X = the InternalRel of N holds

X is closed

then A3: D is closed by YELLOW12:46;

A4: 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:58;

let X be Subset of [:N,N:]; :: thesis: ( X = the InternalRel of N implies X is closed )

assume A5: X = the InternalRel of N ; :: thesis: X is closed

A6: for x, y being Element of N holds f . [x,y] = [x,(x "/\" y)]

N is topological_semilattice by A1, Th22;

then A20: INF is continuous ;

pr1 ( the carrier of N, the carrier of N) is continuous Function of [:N,N:],N by YELLOW12:39;

then f is continuous by A20, YELLOW12:41;

hence X is closed by A9, A3; :: thesis: verum

end;set INF = inf_op N;

set f = <:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):>;

assume N is Hausdorff ; :: thesis: for X being Subset of [:N,N:] st X = the InternalRel of N holds

X is closed

then A3: D is closed by YELLOW12:46;

A4: 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:58;

let X be Subset of [:N,N:]; :: thesis: ( X = the InternalRel of N implies X is closed )

assume A5: X = the InternalRel of N ; :: thesis: X is closed

A6: for x, y being Element of N holds f . [x,y] = [x,(x "/\" y)]

proof

A9:
X = f " D
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: [x,y] in [: the carrier of N, the carrier of N:] by ZFMISC_1:87;

dom (inf_op N) = [: the carrier of N, the carrier of N:] by A4, FUNCT_2:def 1;

hence f . [x,y] = [((pr1 ( the carrier of N, the carrier of N)) . (x,y)),((inf_op N) . (x,y))] by A8, A7, FUNCT_3:49

.= [x,((inf_op N) . (x,y))] by FUNCT_3:def 4

.= [x,(x "/\" y)] by WAYBEL_2:def 4 ;

:: thesis: verum

end;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: [x,y] in [: the carrier of N, the carrier of N:] by ZFMISC_1:87;

dom (inf_op N) = [: the carrier of N, the carrier of N:] by A4, FUNCT_2:def 1;

hence f . [x,y] = [((pr1 ( the carrier of N, the carrier of N)) . (x,y)),((inf_op N) . (x,y))] by A8, A7, FUNCT_3:49

.= [x,((inf_op N) . (x,y))] by FUNCT_3:def 4

.= [x,(x "/\" y)] by WAYBEL_2:def 4 ;

:: thesis: verum

proof

assume A15: a in f " D ; :: thesis: a in X

then A16: f . a in D by FUNCT_1:def 7;

consider s, t being object such that

A17: s in the carrier of N and

A18: t in the carrier of N and

A19: a = [s,t] by A2, A15, ZFMISC_1:def 2;

reconsider s = s, t = t as Element of N by A17, A18;

f . a = [s,(s "/\" t)] by A6, A19;

then s = s "/\" t by A16, RELAT_1:def 10;

then s <= t by YELLOW_0:25;

hence a in X by A5, A19, ORDERS_2:def 5; :: thesis: verum

end;

reconsider INF = inf_op N as Function of [:N,N:],N by A2, A4;hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: f " D c= X

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f " D or a in X )let a be object ; :: thesis: ( a in X implies a in f " D )

assume A10: a in X ; :: thesis: a in f " D

then consider s, t being object such that

A11: s in the carrier of N and

A12: t in the carrier of N and

A13: a = [s,t] by A5, ZFMISC_1:def 2;

reconsider s = s, t = t as Element of N by A11, A12;

s <= t by A5, A10, A13, ORDERS_2:def 5;

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, A11, A12, A13, ZFMISC_1:87;

hence a in f " D by A14, FUNCT_1:def 7; :: thesis: verum

end;assume A10: a in X ; :: thesis: a in f " D

then consider s, t being object such that

A11: s in the carrier of N and

A12: t in the carrier of N and

A13: a = [s,t] by A5, ZFMISC_1:def 2;

reconsider s = s, t = t as Element of N by A11, A12;

s <= t by A5, A10, A13, ORDERS_2:def 5;

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, A11, A12, A13, ZFMISC_1:87;

hence a in f " D by A14, FUNCT_1:def 7; :: thesis: verum

assume A15: a in f " D ; :: thesis: a in X

then A16: f . a in D by FUNCT_1:def 7;

consider s, t being object such that

A17: s in the carrier of N and

A18: t in the carrier of N and

A19: a = [s,t] by A2, A15, ZFMISC_1:def 2;

reconsider s = s, t = t as Element of N by A17, A18;

f . a = [s,(s "/\" t)] by A6, A19;

then s = s "/\" t by A16, RELAT_1:def 10;

then s <= t by YELLOW_0:25;

hence a in X by A5, A19, ORDERS_2:def 5; :: thesis: verum

N is topological_semilattice by A1, Th22;

then A20: INF is continuous ;

pr1 ( the carrier of N, the carrier of N) is continuous Function of [:N,N:],N by YELLOW12:39;

then f is continuous by A20, YELLOW12:41;

hence X is closed by A9, A3; :: thesis: verum

X is closed ; :: thesis: N is Hausdorff

A22: the InternalRel of N /\ the InternalRel of (N ~) c= id the carrier of N by YELLOW12:23;

id the carrier of N c= the InternalRel of N /\ the InternalRel of (N ~) by YELLOW12:22;

then A23: id the carrier of N = the InternalRel of N /\ the InternalRel of (N ~) by A22;

for A being Subset of [:N,N:] st A = id the carrier of N holds

A is closed

proof

hence
N is Hausdorff
by YELLOW12:46; :: thesis: verum
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;

reconsider X = the InternalRel of N, Y = the InternalRel of (N ~) as Subset of [:N,N:] by BORSUK_1:def 2;

let A be Subset of [:N,N:]; :: thesis: ( A = id the carrier of N implies A is closed )

assume A24: A = id the carrier of N ; :: thesis: A is closed

reconsider X = X, Y = Y as Subset of [:N,N:] ;

A25: X is closed by A21;

A26: dom f = [: the carrier of N, the carrier of N:] by YELLOW12:4;

A27: f .: X = Y

then Y is closed by A25, A27, TOPS_2:58;

hence A is closed by A23, A24, A25; :: thesis: verum

end;reconsider X = the InternalRel of N, Y = the InternalRel of (N ~) as Subset of [:N,N:] by BORSUK_1:def 2;

let A be Subset of [:N,N:]; :: thesis: ( A = id the carrier of N implies A is closed )

assume A24: A = id the carrier of N ; :: thesis: A is closed

reconsider X = X, Y = Y as Subset of [:N,N:] ;

A25: X is closed by A21;

A26: dom f = [: the carrier of N, the carrier of N:] by YELLOW12:4;

A27: f .: X = Y

proof

f is being_homeomorphism
by YELLOW12:43;
thus
f .: X c= Y
:: according to XBOOLE_0:def 10 :: thesis: Y c= f .: X

assume A33: y in Y ; :: thesis: y in f .: X

then consider y1, y2 being object such that

A34: y1 in the carrier of N and

A35: y2 in the carrier of N and

A36: y = [y1,y2] by ZFMISC_1:def 2;

A37: [y2,y1] in X by A33, A36, RELAT_1:def 7;

f . [y2,y1] = y by A34, A35, A36, Lm3;

hence y in f .: X by A26, A37, FUNCT_1:def 6; :: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in f .: X )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: X or y in Y )

assume y in f .: X ; :: thesis: y in Y

then consider x being object such that

x in dom f and

A28: x in X and

A29: y = f . x by FUNCT_1:def 6;

consider x1, x2 being object such that

A30: x1 in the carrier of N and

A31: x2 in the carrier of N and

A32: x = [x1,x2] by A28, ZFMISC_1:def 2;

f . x = [x2,x1] by A30, A31, A32, Lm3;

hence y in Y by A28, A29, A32, RELAT_1:def 7; :: thesis: verum

end;assume y in f .: X ; :: thesis: y in Y

then consider x being object such that

x in dom f and

A28: x in X and

A29: y = f . x by FUNCT_1:def 6;

consider x1, x2 being object such that

A30: x1 in the carrier of N and

A31: x2 in the carrier of N and

A32: x = [x1,x2] by A28, ZFMISC_1:def 2;

f . x = [x2,x1] by A30, A31, A32, Lm3;

hence y in Y by A28, A29, A32, RELAT_1:def 7; :: thesis: verum

assume A33: y in Y ; :: thesis: y in f .: X

then consider y1, y2 being object such that

A34: y1 in the carrier of N and

A35: y2 in the carrier of N and

A36: y = [y1,y2] by ZFMISC_1:def 2;

A37: [y2,y1] in X by A33, A36, RELAT_1:def 7;

f . [y2,y1] = y by A34, A35, A36, Lm3;

hence y in f .: X by A26, A37, FUNCT_1:def 6; :: thesis: verum

then Y is closed by A25, A27, TOPS_2:58;

hence A is closed by A23, A24, A25; :: thesis: verum