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;

hereby :: thesis: ( ( 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)]

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: [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;

A9: X = f " D

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: f " D c= 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;

let a be object ; :: 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: 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;
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;

assume A21: for X being Subset of [:N,N:] st X = the InternalRel of N holds
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

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

proof

thus f .: X c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= f .: X

proof

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;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in 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;

f is being_homeomorphism by YELLOW12:43;
then Y is closed by A25, A27, TOPS_2:58;
hence A is closed by A23, A24, A25; :: thesis: verum

end;

hence N is Hausdorff by YELLOW12:46; :: thesis: verum