let S be Hausdorff compact TopLattice; :: thesis:
let N be net of S; :: thesis:
let c be Point of S; :: thesis:
let d be Element of S; :: thesis:
assume that
A1: c = d and
A2: for x being Element of S holds x "/\" is continuous and
A3: N is eventually-directed and
A4: c is_a_cluster_point_of N ; :: thesis:
let i be Element of S; :: according to LATTICE3:def 9 :: thesis:
assume i in rng the mapping of N ; :: thesis:
then consider iJ being set such that
A5: iJ in dom the mapping of N and
A6: the mapping of N . iJ = i by FUNCT_1:def 5;
reconsider i1 = iJ as Element of N by A5;
A7: uparrow (N . i1) = { z where z is Element of S : z "/\" (N . i1) = N . i1 } by Lm1;
A8: N is_eventually_in uparrow (N . i1)

consider j being Element of N such that
A9: for k being Element of N st j <= k holds
N . i1 <= N . k by A3, WAYBEL_0:11;
take j ; :: according to WAYBEL_0:def 11 :: thesis:
let k be Element of N; :: thesis:
assume j <= k ; :: thesis:
then N . i1 <= N . k by A9;
hence N . k in uparrow (N . i1) by WAYBEL_0:18; :: thesis:

end;

uparrow (N . i1) is closed by A2, Th27;
then A10: Cl (uparrow (N . i1)) = uparrow (N . i1) by PRE_TOPC:52;
consider t being Element of N such that
A11: for j being Element of N st t <= j holds
N . j in uparrow (N . i1) by A8, WAYBEL_0:def 11;
reconsider A = N | t as subnet of N ;
A12: rng the mapping of A c= uparrow (N . i1)

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume q in rng the mapping of A ; :: thesis:
then consider x being set such that
A13: x in dom the mapping of A and
A14: q = the mapping of A . x by FUNCT_1:def 5;
reconsider x = x as Element of A by A13;
consider y being Element of N such that
A15: y = x and
A16: t <= y by Def7;
A . x = N . y by A15, Th16;
hence q in uparrow (N . i1) by A11, A14, A16; :: thesis:

end;

c is_a_cluster_point_of A

let O be a_neighborhood of c; :: according to WAYBEL_9:def 9 :: thesis:
let i be Element of A; :: according to WAYBEL_0:def 12 :: thesis:
consider i2 being Element of N such that
A17: i2 = i and
A18: t <= i2 by Def7;
N is_often_in O by A4, Def9;
then consider j2 being Element of N such that
A19: i2 <= j2 and
A20: N . j2 in O by WAYBEL_0:def 12;
t <= j2 by A18, A19, YELLOW_0:def 2;
then reconsider j = j2 as Element of A by Def7;
take j ; :: thesis:
A is full SubNetStr of N by Th14;
hence i <= j by A17, A19, YELLOW_6:21; :: thesis:
thus A . j in O by A20, Th16; :: thesis:

end;

then consider M being subnet of A such that
A21: c in Lim M by Th32;
consider f being Function of M,A such that
A22: the mapping of M = the mapping of A * f and
for m being Element of A ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p by YELLOW_6:def 12;
reconsider R = rng the mapping of M as Subset of S ;
R c= rng the mapping of A by A22, RELAT_1:45;
then R c= uparrow (N . i1) by A12, XBOOLE_1:1;
then A23: Cl R c= Cl (uparrow (N . i1)) by PRE_TOPC:49;
c in Cl R by A21, Th24;
then c in uparrow (N . i1) by A10, A23;
then consider z being Element of S such that
A24: ( c = z & z "/\" (N . i1) = N . i1 ) by A7;
thus i <= d by A1, A6, A24, YELLOW_0:25; :: thesis: