let N be complete Lawson meet-continuous TopLattice; :: thesis: ( InclPoset () 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 () 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)),():>;
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)),():> as Function of [:N,N:],[:N,N:] by ;
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 () = [: the carrier of N, the carrier of N:] by ;
hence f . [x,y] = [((pr1 ( the carrier of N, the carrier of N)) . (x,y)),(() . (x,y))] by
.= [x,(() . (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 ;
reconsider s = s, t = t as Element of N by ;
s <= t by ;
then s "/\" t = s by YELLOW_0:25;
then f . [s,t] = [s,s] by A6;
then A14: f . a in D by ;
dom f = the carrier of [:N,N:] by FUNCT_2:def 1;
then a in dom f by ;
hence a in f " D by ; :: 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 ;
reconsider s = s, t = t as Element of N by ;
f . a = [s,(s "/\" t)] by ;
then s = s "/\" t by ;
then s <= t by YELLOW_0:25;
hence a in X by ; :: thesis: verum
end;
reconsider INF = inf_op N as Function of [:N,N:],N by A2, A4;
N is topological_semilattice by ;
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 ;
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 ;
f . x = [x2,x1] by A30, A31, A32, Lm3;
hence y in Y by ; :: 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 ;
f . [y2,y1] = y by A34, A35, A36, Lm3;
hence y in f .: X by ; :: thesis: verum
end;
f is being_homeomorphism by YELLOW12:43;
then Y is closed by ;
hence A is closed by ; :: thesis: verum
end;
hence N is Hausdorff by YELLOW12:46; :: thesis: verum