:: WAYBEL_9 semantic presentation begin registration let L be non empty RelStr ; cluster id L -> monotone ; coherence id L is monotone by YELLOW_2:11; end; definition let S, T be non empty RelStr ; let f be Function of S,T; redefine attr f is antitone means :Def1: :: WAYBEL_9:def 1 for x, y being Element of S st x <= y holds f . x >= f . y; compatibility ( f is antitone iff for x, y being Element of S st x <= y holds f . x >= f . y ) proof thus ( f is antitone implies for x, y being Element of S st x <= y holds f . x >= f . y ) by WAYBEL_0:def_5; ::_thesis: ( ( for x, y being Element of S st x <= y holds f . x >= f . y ) implies f is antitone ) assume for x, y being Element of S st x <= y holds f . x >= f . y ; ::_thesis: f is antitone hence for x, y being Element of S st x <= y holds for a, b being Element of T st a = f . x & b = f . y holds a >= b ; :: according to WAYBEL_0:def_5 ::_thesis: verum end; end; :: deftheorem Def1 defines antitone WAYBEL_9:def_1_:_ for S, T being non empty RelStr for f being Function of S,T holds ( f is antitone iff for x, y being Element of S st x <= y holds f . x >= f . y ); theorem Th1: :: WAYBEL_9:1 for S, T being RelStr for K, L being non empty RelStr for f being Function of S,T for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds g is monotone proof let S, T be RelStr ; ::_thesis: for K, L being non empty RelStr for f being Function of S,T for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds g is monotone let K, L be non empty RelStr ; ::_thesis: for f being Function of S,T for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds g is monotone let f be Function of S,T; ::_thesis: for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds g is monotone let g be Function of K,L; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone implies g is monotone ) assume that A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) and A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) and A3: f = g and A4: f is monotone ; ::_thesis: g is monotone reconsider S1 = S, T1 = T as non empty RelStr by A1, A2; let x, y be Element of K; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or g . x <= g . y ) assume A5: x <= y ; ::_thesis: g . x <= g . y reconsider x1 = x, y1 = y as Element of S1 by A1; reconsider f1 = f as Function of S1,T1 ; x1 <= y1 by A1, A5, YELLOW_0:1; then f1 . x1 <= f1 . y1 by A4, WAYBEL_1:def_2; hence g . x <= g . y by A2, A3, YELLOW_0:1; ::_thesis: verum end; theorem Th2: :: WAYBEL_9:2 for S, T being RelStr for K, L being non empty RelStr for f being Function of S,T for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds g is antitone proof let S, T be RelStr ; ::_thesis: for K, L being non empty RelStr for f being Function of S,T for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds g is antitone let K, L be non empty RelStr ; ::_thesis: for f being Function of S,T for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds g is antitone let f be Function of S,T; ::_thesis: for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds g is antitone let g be Function of K,L; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone implies g is antitone ) assume that A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) and A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) and A3: f = g and A4: f is antitone ; ::_thesis: g is antitone reconsider S1 = S, T1 = T as non empty RelStr by A1, A2; let x, y be Element of K; :: according to WAYBEL_9:def_1 ::_thesis: ( x <= y implies g . x >= g . y ) assume A5: x <= y ; ::_thesis: g . x >= g . y reconsider x1 = x, y1 = y as Element of S1 by A1; reconsider f1 = f as Function of S1,T1 ; x1 <= y1 by A1, A5, YELLOW_0:1; then f1 . x1 >= f1 . y1 by A4, Def1; hence g . x >= g . y by A2, A3, YELLOW_0:1; ::_thesis: verum end; theorem :: WAYBEL_9:3 for A, B being 1-sorted for F being Subset-Family of A for G being Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover of A holds G is Cover of B ; Lm1: for L being reflexive antisymmetric with_infima RelStr for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x } proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x } let x be Element of L; ::_thesis: uparrow x = { z where z is Element of L : z "/\" x = x } thus uparrow x c= { z where z is Element of L : z "/\" x = x } :: according to XBOOLE_0:def_10 ::_thesis: { z where z is Element of L : z "/\" x = x } c= uparrow x proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow x or q in { z where z is Element of L : z "/\" x = x } ) assume A1: q in uparrow x ; ::_thesis: q in { z where z is Element of L : z "/\" x = x } then reconsider q1 = q as Element of L ; x <= q1 by A1, WAYBEL_0:18; then q1 "/\" x = x by YELLOW_0:25; hence q in { z where z is Element of L : z "/\" x = x } ; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { z where z is Element of L : z "/\" x = x } or q in uparrow x ) assume q in { z where z is Element of L : z "/\" x = x } ; ::_thesis: q in uparrow x then consider z being Element of L such that A2: q = z and A3: z "/\" x = x ; x <= z by A3, YELLOW_0:25; hence q in uparrow x by A2, WAYBEL_0:18; ::_thesis: verum end; theorem Th4: :: WAYBEL_9:4 for L being reflexive antisymmetric with_suprema RelStr for x being Element of L holds uparrow x = {x} "\/" ([#] L) proof let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for x being Element of L holds uparrow x = {x} "\/" ([#] L) let x be Element of L; ::_thesis: uparrow x = {x} "\/" ([#] L) A1: {x} "\/" ([#] L) = { (x "\/" s) where s is Element of L : s in [#] L } by YELLOW_4:15; thus uparrow x c= {x} "\/" ([#] L) :: according to XBOOLE_0:def_10 ::_thesis: {x} "\/" ([#] L) c= uparrow x proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow x or q in {x} "\/" ([#] L) ) assume A2: q in uparrow x ; ::_thesis: q in {x} "\/" ([#] L) then reconsider q1 = q as Element of L ; x <= q1 by A2, WAYBEL_0:18; then x "\/" q1 = q1 by YELLOW_0:24; hence q in {x} "\/" ([#] L) by A1; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "\/" ([#] L) or q in uparrow x ) assume q in {x} "\/" ([#] L) ; ::_thesis: q in uparrow x then consider z being Element of L such that A3: q = x "\/" z and z in [#] L by A1; x <= x "\/" z by YELLOW_0:22; hence q in uparrow x by A3, WAYBEL_0:18; ::_thesis: verum end; Lm2: for L being reflexive antisymmetric with_suprema RelStr for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x } proof let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x } let x be Element of L; ::_thesis: downarrow x = { z where z is Element of L : z "\/" x = x } thus downarrow x c= { z where z is Element of L : z "\/" x = x } :: according to XBOOLE_0:def_10 ::_thesis: { z where z is Element of L : z "\/" x = x } c= downarrow x proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow x or q in { z where z is Element of L : z "\/" x = x } ) assume A1: q in downarrow x ; ::_thesis: q in { z where z is Element of L : z "\/" x = x } then reconsider q1 = q as Element of L ; x >= q1 by A1, WAYBEL_0:17; then q1 "\/" x = x by YELLOW_0:24; hence q in { z where z is Element of L : z "\/" x = x } ; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { z where z is Element of L : z "\/" x = x } or q in downarrow x ) assume q in { z where z is Element of L : z "\/" x = x } ; ::_thesis: q in downarrow x then consider z being Element of L such that A2: q = z and A3: z "\/" x = x ; x >= z by A3, YELLOW_0:24; hence q in downarrow x by A2, WAYBEL_0:17; ::_thesis: verum end; theorem Th5: :: WAYBEL_9:5 for L being reflexive antisymmetric with_infima RelStr for x being Element of L holds downarrow x = {x} "/\" ([#] L) proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for x being Element of L holds downarrow x = {x} "/\" ([#] L) let x be Element of L; ::_thesis: downarrow x = {x} "/\" ([#] L) A1: {x} "/\" ([#] L) = { (x "/\" s) where s is Element of L : s in [#] L } by YELLOW_4:42; thus downarrow x c= {x} "/\" ([#] L) :: according to XBOOLE_0:def_10 ::_thesis: {x} "/\" ([#] L) c= downarrow x proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow x or q in {x} "/\" ([#] L) ) assume A2: q in downarrow x ; ::_thesis: q in {x} "/\" ([#] L) then reconsider q1 = q as Element of L ; x >= q1 by A2, WAYBEL_0:17; then x "/\" q1 = q1 by YELLOW_0:25; hence q in {x} "/\" ([#] L) by A1; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "/\" ([#] L) or q in downarrow x ) assume q in {x} "/\" ([#] L) ; ::_thesis: q in downarrow x then consider z being Element of L such that A3: q = x "/\" z and z in [#] L by A1; x "/\" z <= x by YELLOW_0:23; hence q in downarrow x by A3, WAYBEL_0:17; ::_thesis: verum end; theorem :: WAYBEL_9:6 for L being reflexive antisymmetric with_infima RelStr for y being Element of L holds (y "/\") .: (uparrow y) = {y} proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for y being Element of L holds (y "/\") .: (uparrow y) = {y} let y be Element of L; ::_thesis: (y "/\") .: (uparrow y) = {y} thus (y "/\") .: (uparrow y) c= {y} :: according to XBOOLE_0:def_10 ::_thesis: {y} c= (y "/\") .: (uparrow y) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (y "/\") .: (uparrow y) or q in {y} ) assume q in (y "/\") .: (uparrow y) ; ::_thesis: q in {y} then consider a being set such that a in dom (y "/\") and A1: a in uparrow y and A2: q = (y "/\") . a by FUNCT_1:def_6; reconsider a = a as Element of L by A1; A3: y <= a by A1, WAYBEL_0:18; q = y "/\" a by A2, WAYBEL_1:def_18 .= y by A3, YELLOW_0:25 ; hence q in {y} by TARSKI:def_1; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {y} or q in (y "/\") .: (uparrow y) ) assume q in {y} ; ::_thesis: q in (y "/\") .: (uparrow y) then A4: q = y by TARSKI:def_1; y <= y ; then A5: ( dom (y "/\") = the carrier of L & y in uparrow y ) by FUNCT_2:def_1, WAYBEL_0:18; y = y "/\" y by YELLOW_0:25 .= (y "/\") . y by WAYBEL_1:def_18 ; hence q in (y "/\") .: (uparrow y) by A4, A5, FUNCT_1:def_6; ::_thesis: verum end; theorem Th7: :: WAYBEL_9:7 for L being reflexive antisymmetric with_infima RelStr for x being Element of L holds (x "/\") " {x} = uparrow x proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for x being Element of L holds (x "/\") " {x} = uparrow x let x be Element of L; ::_thesis: (x "/\") " {x} = uparrow x thus (x "/\") " {x} c= uparrow x :: according to XBOOLE_0:def_10 ::_thesis: uparrow x c= (x "/\") " {x} proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (x "/\") " {x} or q in uparrow x ) assume A1: q in (x "/\") " {x} ; ::_thesis: q in uparrow x then reconsider q1 = q as Element of L ; A2: (x "/\") . q1 in {x} by A1, FUNCT_1:def_7; x "/\" q1 = (x "/\") . q1 by WAYBEL_1:def_18 .= x by A2, TARSKI:def_1 ; then x <= q1 by YELLOW_0:25; hence q in uparrow x by WAYBEL_0:18; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow x or q in (x "/\") " {x} ) assume A3: q in uparrow x ; ::_thesis: q in (x "/\") " {x} then reconsider q1 = q as Element of L ; A4: x <= q1 by A3, WAYBEL_0:18; (x "/\") . q1 = x "/\" q1 by WAYBEL_1:def_18 .= x by A4, YELLOW_0:25 ; then ( dom (x "/\") = the carrier of L & (x "/\") . q1 in {x} ) by FUNCT_2:def_1, TARSKI:def_1; hence q in (x "/\") " {x} by FUNCT_1:def_7; ::_thesis: verum end; theorem Th8: :: WAYBEL_9:8 for T being non empty 1-sorted for N being non empty NetStr over T holds N is_eventually_in rng the mapping of N proof let T be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over T holds N is_eventually_in rng the mapping of N let N be non empty NetStr over T; ::_thesis: N is_eventually_in rng the mapping of N set i = the Element of N; take the Element of N ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not the Element of N <= b1 or N . b1 in rng the mapping of N ) let j be Element of N; ::_thesis: ( not the Element of N <= j or N . j in rng the mapping of N ) assume the Element of N <= j ; ::_thesis: N . j in rng the mapping of N thus N . j in rng the mapping of N by FUNCT_2:4; ::_thesis: verum end; Lm3: for L being non empty reflexive transitive RelStr for D being non empty directed Subset of L for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L proof let L be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of L for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L let D be non empty directed Subset of L; ::_thesis: for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L let n be Function of D, the carrier of L; ::_thesis: NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L set N = NetStr(# D,( the InternalRel of L |_2 D),n #); the InternalRel of NetStr(# D,( the InternalRel of L |_2 D),n #) c= the InternalRel of L by XBOOLE_1:17; then reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as SubRelStr of L by YELLOW_0:def_13; reconsider N = N as full SubRelStr of L by YELLOW_0:def_14; N is directed proof let x, y be Element of N; :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] N or not y in [#] N or ex b1 being Element of the carrier of N st ( b1 in [#] N & x <= b1 & y <= b1 ) ) assume that x in [#] N and y in [#] N ; ::_thesis: ex b1 being Element of the carrier of N st ( b1 in [#] N & x <= b1 & y <= b1 ) reconsider x1 = x, y1 = y as Element of D ; consider z1 being Element of L such that A1: z1 in D and A2: ( x1 <= z1 & y1 <= z1 ) by WAYBEL_0:def_1; reconsider z = z1 as Element of N by A1; take z ; ::_thesis: ( z in [#] N & x <= z & y <= z ) thus z in [#] N ; ::_thesis: ( x <= z & y <= z ) thus ( x <= z & y <= z ) by A2, YELLOW_0:60; ::_thesis: verum end; then reconsider N = N as prenet of L ; N is transitive ; hence NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L ; ::_thesis: verum end; registration let L be non empty reflexive RelStr ; let D be non empty directed Subset of L; let n be Function of D, the carrier of L; cluster NetStr(# D,( the InternalRel of L |_2 D),n #) -> directed ; coherence NetStr(# D,( the InternalRel of L |_2 D),n #) is directed by WAYBEL_2:19; end; registration let L be non empty reflexive transitive RelStr ; let D be non empty directed Subset of L; let n be Function of D, the carrier of L; cluster NetStr(# D,( the InternalRel of L |_2 D),n #) -> transitive ; coherence NetStr(# D,( the InternalRel of L |_2 D),n #) is transitive by Lm3; end; theorem Th9: :: WAYBEL_9:9 for L being non empty reflexive transitive RelStr st ( for x being Element of L for N being net of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds L is satisfying_MC proof let L be non empty reflexive transitive RelStr ; ::_thesis: ( ( for x being Element of L for N being net of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies L is satisfying_MC ) assume A1: for x being Element of L for N being net of L st N is eventually-directed holds x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; ::_thesis: L is satisfying_MC let x be Element of L; :: according to WAYBEL_2:def_6 ::_thesis: for b1 being Element of K10( the carrier of L) holds x "/\" ("\/" (b1,L)) = "\/" (({x} "/\" b1),L) let D be non empty directed Subset of L; ::_thesis: x "/\" ("\/" (D,L)) = "\/" (({x} "/\" D),L) reconsider n = id D as Function of D, the carrier of L by FUNCT_2:7; set N = NetStr(# D,( the InternalRel of L |_2 D),n #); A2: ( NetStr(# D,( the InternalRel of L |_2 D),n #) is eventually-directed & Sup = sup NetStr(# D,( the InternalRel of L |_2 D),n #) ) by WAYBEL_2:20; D c= D ; then A3: D = n .: D by FUNCT_1:92 .= rng (netmap (NetStr(# D,( the InternalRel of L |_2 D),n #),L)) by RELSET_1:22 ; hence x "/\" (sup D) = x "/\" (Sup ) by YELLOW_2:def_5 .= sup ({x} "/\" D) by A1, A3, A2 ; ::_thesis: verum end; theorem Th10: :: WAYBEL_9:10 for L being non empty RelStr for a being Element of L for N being net of L holds a "/\" N is net of L proof let L be non empty RelStr ; ::_thesis: for a being Element of L for N being net of L holds a "/\" N is net of L let a be Element of L; ::_thesis: for N being net of L holds a "/\" N is net of L let N be net of L; ::_thesis: a "/\" N is net of L set aN = a "/\" N; a "/\" N is transitive proof let x, y, z be Element of (a "/\" N); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume A1: ( x <= y & y <= z ) ; ::_thesis: x <= z reconsider x1 = x, y1 = y, z1 = z as Element of N by WAYBEL_2:22; A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (a "/\" N), the InternalRel of (a "/\" N) #) by WAYBEL_2:def_3; then ( x1 <= y1 & y1 <= z1 ) by A1, YELLOW_0:1; then x1 <= z1 by YELLOW_0:def_2; hence x <= z by A2, YELLOW_0:1; ::_thesis: verum end; hence a "/\" N is net of L ; ::_thesis: verum end; registration let L be non empty RelStr ; let x be Element of L; let N be net of L; clusterx "/\" N -> transitive ; coherence x "/\" N is transitive by Th10; end; registration let L be non empty RelStr ; let x be Element of L; let N be non empty reflexive NetStr over L; clusterx "/\" N -> reflexive ; coherence x "/\" N is reflexive proof RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3; then the InternalRel of (x "/\" N) is_reflexive_in the carrier of (x "/\" N) by ORDERS_2:def_2; hence x "/\" N is reflexive by ORDERS_2:def_2; ::_thesis: verum end; end; registration let L be non empty RelStr ; let x be Element of L; let N be non empty antisymmetric NetStr over L; clusterx "/\" N -> antisymmetric ; coherence x "/\" N is antisymmetric proof RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3; then the InternalRel of (x "/\" N) is_antisymmetric_in the carrier of (x "/\" N) by ORDERS_2:def_4; hence x "/\" N is antisymmetric by ORDERS_2:def_4; ::_thesis: verum end; end; registration let L be non empty RelStr ; let x be Element of L; let N be non empty transitive NetStr over L; clusterx "/\" N -> transitive ; coherence x "/\" N is transitive proof RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3; then the InternalRel of (x "/\" N) is_transitive_in the carrier of (x "/\" N) by ORDERS_2:def_3; hence x "/\" N is transitive by ORDERS_2:def_3; ::_thesis: verum end; end; registration let L be non empty RelStr ; let J be set ; let f be Function of J, the carrier of L; cluster FinSups f -> transitive ; coherence FinSups f is transitive proof let x, y, z be Element of (FinSups f); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume that A1: x <= y and A2: y <= z ; ::_thesis: x <= z A3: ( ex g being Function of (Fin J), the carrier of L st for x being Element of Fin J holds ( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) ) by WAYBEL_2:def_2, YELLOW_1:def_1; then reconsider x1 = x, y1 = y, z1 = z as Element of (InclPoset (Fin J)) ; y1 <= z1 by A2, A3, YELLOW_0:1; then A4: y1 c= z1 by YELLOW_1:3; x1 <= y1 by A1, A3, YELLOW_0:1; then x1 c= y1 by YELLOW_1:3; then x1 c= z1 by A4, XBOOLE_1:1; then x1 <= z1 by YELLOW_1:3; hence x <= z by A3, YELLOW_0:1; ::_thesis: verum end; end; begin definition let L be non empty RelStr ; let N be NetStr over L; func inf N -> Element of L equals :: WAYBEL_9:def 2 Inf ; coherence Inf is Element of L ; end; :: deftheorem defines inf WAYBEL_9:def_2_:_ for L being non empty RelStr for N being NetStr over L holds inf N = Inf ; definition let L be RelStr ; let N be NetStr over L; pred ex_sup_of N means :Def3: :: WAYBEL_9:def 3 ex_sup_of rng the mapping of N,L; pred ex_inf_of N means :Def4: :: WAYBEL_9:def 4 ex_inf_of rng the mapping of N,L; end; :: deftheorem Def3 defines ex_sup_of WAYBEL_9:def_3_:_ for L being RelStr for N being NetStr over L holds ( ex_sup_of N iff ex_sup_of rng the mapping of N,L ); :: deftheorem Def4 defines ex_inf_of WAYBEL_9:def_4_:_ for L being RelStr for N being NetStr over L holds ( ex_inf_of N iff ex_inf_of rng the mapping of N,L ); definition let L be RelStr ; funcL +id -> strict NetStr over L means :Def5: :: WAYBEL_9:def 5 ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of it = id L ); existence ex b1 being strict NetStr over L st ( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b1 = id L ) proof take NetStr(# the carrier of L, the InternalRel of L,(id L) #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of L, the InternalRel of L,(id L) #), the InternalRel of NetStr(# the carrier of L, the InternalRel of L,(id L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of NetStr(# the carrier of L, the InternalRel of L,(id L) #) = id L ) thus ( RelStr(# the carrier of NetStr(# the carrier of L, the InternalRel of L,(id L) #), the InternalRel of NetStr(# the carrier of L, the InternalRel of L,(id L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of NetStr(# the carrier of L, the InternalRel of L,(id L) #) = id L ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b1 = id L & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b2 = id L holds b1 = b2 ; end; :: deftheorem Def5 defines +id WAYBEL_9:def_5_:_ for L being RelStr for b2 being strict NetStr over L holds ( b2 = L +id iff ( RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b2 = id L ) ); registration let L be non empty RelStr ; clusterL +id -> non empty strict ; coherence not L +id is empty proof RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5; hence not L +id is empty ; ::_thesis: verum end; end; registration let L be reflexive RelStr ; clusterL +id -> reflexive strict ; coherence L +id is reflexive proof RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5; then the InternalRel of (L +id) is_reflexive_in the carrier of (L +id) by ORDERS_2:def_2; hence L +id is reflexive by ORDERS_2:def_2; ::_thesis: verum end; end; registration let L be antisymmetric RelStr ; clusterL +id -> antisymmetric strict ; coherence L +id is antisymmetric proof RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5; then the InternalRel of (L +id) is_antisymmetric_in the carrier of (L +id) by ORDERS_2:def_4; hence L +id is antisymmetric by ORDERS_2:def_4; ::_thesis: verum end; end; registration let L be transitive RelStr ; clusterL +id -> transitive strict ; coherence L +id is transitive proof RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5; then the InternalRel of (L +id) is_transitive_in the carrier of (L +id) by ORDERS_2:def_3; hence L +id is transitive by ORDERS_2:def_3; ::_thesis: verum end; end; registration let L be with_suprema RelStr ; clusterL +id -> strict directed ; coherence L +id is directed proof A1: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5; then [#] L = [#] (L +id) ; hence [#] (L +id) is directed by A1, WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum end; end; registration let L be directed RelStr ; clusterL +id -> strict directed ; coherence L +id is directed proof ( [#] L is directed & RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) ) by Def5, WAYBEL_0:def_6; hence [#] (L +id) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum end; end; registration let L be non empty RelStr ; clusterL +id -> strict monotone eventually-directed ; coherence ( L +id is monotone & L +id is eventually-directed ) proof set N = L +id ; ( netmap ((L +id),L) = id L & RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by Def5; then netmap ((L +id),L) is monotone by Th1; hence L +id is monotone by WAYBEL_0:def_9; ::_thesis: L +id is eventually-directed for i being Element of (L +id) ex j being Element of (L +id) st for k being Element of (L +id) st j <= k holds (L +id) . i <= (L +id) . k proof let i be Element of (L +id); ::_thesis: ex j being Element of (L +id) st for k being Element of (L +id) st j <= k holds (L +id) . i <= (L +id) . k take j = i; ::_thesis: for k being Element of (L +id) st j <= k holds (L +id) . i <= (L +id) . k let k be Element of (L +id); ::_thesis: ( j <= k implies (L +id) . i <= (L +id) . k ) assume A1: j <= k ; ::_thesis: (L +id) . i <= (L +id) . k A2: RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) = RelStr(# the carrier of L, the InternalRel of L #) by Def5; the mapping of (L +id) = id L by Def5; then ( the mapping of (L +id) . i = i & the mapping of (L +id) . k = k ) by A2, FUNCT_1:18; hence (L +id) . i <= (L +id) . k by A1, A2, YELLOW_0:1; ::_thesis: verum end; hence L +id is eventually-directed by WAYBEL_0:11; ::_thesis: verum end; end; definition let L be RelStr ; funcL opp+id -> strict NetStr over L means :Def6: :: WAYBEL_9:def 6 ( the carrier of it = the carrier of L & the InternalRel of it = the InternalRel of L ~ & the mapping of it = id L ); existence ex b1 being strict NetStr over L st ( the carrier of b1 = the carrier of L & the InternalRel of b1 = the InternalRel of L ~ & the mapping of b1 = id L ) proof take NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) ; ::_thesis: ( the carrier of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = the carrier of L & the InternalRel of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = the InternalRel of L ~ & the mapping of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = id L ) thus ( the carrier of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = the carrier of L & the InternalRel of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = the InternalRel of L ~ & the mapping of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = id L ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict NetStr over L st the carrier of b1 = the carrier of L & the InternalRel of b1 = the InternalRel of L ~ & the mapping of b1 = id L & the carrier of b2 = the carrier of L & the InternalRel of b2 = the InternalRel of L ~ & the mapping of b2 = id L holds b1 = b2 ; end; :: deftheorem Def6 defines opp+id WAYBEL_9:def_6_:_ for L being RelStr for b2 being strict NetStr over L holds ( b2 = L opp+id iff ( the carrier of b2 = the carrier of L & the InternalRel of b2 = the InternalRel of L ~ & the mapping of b2 = id L ) ); theorem Th11: :: WAYBEL_9:11 for L being RelStr holds RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) proof let L be RelStr ; ::_thesis: RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) the InternalRel of (L ~) = the InternalRel of (L opp+id) by Def6; hence RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) by Def6; ::_thesis: verum end; registration let L be non empty RelStr ; clusterL opp+id -> non empty strict ; coherence not L opp+id is empty proof RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) by Th11; hence not L opp+id is empty ; ::_thesis: verum end; end; registration let L be reflexive RelStr ; clusterL opp+id -> reflexive strict ; coherence L opp+id is reflexive proof the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def_2; then A1: the InternalRel of L ~ is_reflexive_in the carrier of L by ORDERS_1:79; the InternalRel of (L opp+id) = the InternalRel of L ~ by Def6; hence the InternalRel of (L opp+id) is_reflexive_in the carrier of (L opp+id) by A1, Def6; :: according to ORDERS_2:def_2 ::_thesis: verum end; end; registration let L be antisymmetric RelStr ; clusterL opp+id -> antisymmetric strict ; coherence L opp+id is antisymmetric proof the InternalRel of L is_antisymmetric_in the carrier of L by ORDERS_2:def_4; then A1: the InternalRel of L ~ is_antisymmetric_in the carrier of L by ORDERS_1:81; the InternalRel of (L opp+id) = the InternalRel of L ~ by Def6; then the InternalRel of (L opp+id) is_antisymmetric_in the carrier of (L opp+id) by A1, Def6; hence L opp+id is antisymmetric by ORDERS_2:def_4; ::_thesis: verum end; end; registration let L be transitive RelStr ; clusterL opp+id -> transitive strict ; coherence L opp+id is transitive proof the InternalRel of L is_transitive_in the carrier of L by ORDERS_2:def_3; then A1: the InternalRel of L ~ is_transitive_in the carrier of L by ORDERS_1:80; the InternalRel of (L opp+id) = the InternalRel of L ~ by Def6; then the InternalRel of (L opp+id) is_transitive_in the carrier of (L opp+id) by A1, Def6; hence L opp+id is transitive by ORDERS_2:def_3; ::_thesis: verum end; end; registration let L be with_infima RelStr ; clusterL opp+id -> strict directed ; coherence L opp+id is directed proof reconsider A = L ~ as with_suprema RelStr by YELLOW_7:16; ( RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) & [#] A = [#] (L opp+id) ) by Def6, Th11; hence [#] (L opp+id) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum end; end; registration let L be non empty RelStr ; clusterL opp+id -> strict antitone eventually-filtered ; coherence ( L opp+id is antitone & L opp+id is eventually-filtered ) proof set N = L opp+id ; thus L opp+id is antitone ::_thesis: L opp+id is eventually-filtered proof reconsider f = id L as Function of (L ~),L ; reconsider g = f as Function of L,(L ~) ; g is antitone by YELLOW_7:40; then A1: ( RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of L, the InternalRel of L #) & f is antitone ) by YELLOW_7:41; ( netmap ((L opp+id),L) = id L & RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) = RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) ) by Def6, Th11; hence netmap ((L opp+id),L) is antitone by A1, Th2; :: according to WAYBEL_0:def_10 ::_thesis: verum end; for i being Element of (L opp+id) ex j being Element of (L opp+id) st for k being Element of (L opp+id) st j <= k holds (L opp+id) . i >= (L opp+id) . k proof let i be Element of (L opp+id); ::_thesis: ex j being Element of (L opp+id) st for k being Element of (L opp+id) st j <= k holds (L opp+id) . i >= (L opp+id) . k take j = i; ::_thesis: for k being Element of (L opp+id) st j <= k holds (L opp+id) . i >= (L opp+id) . k A2: ( the mapping of (L opp+id) = id L & the InternalRel of (L opp+id) = the InternalRel of L ~ ) by Def6; let k be Element of (L opp+id); ::_thesis: ( j <= k implies (L opp+id) . i >= (L opp+id) . k ) assume j <= k ; ::_thesis: (L opp+id) . i >= (L opp+id) . k then [i,k] in the InternalRel of (L opp+id) by ORDERS_2:def_5; then A3: [k,i] in the InternalRel of (L opp+id) ~ by RELAT_1:def_7; reconsider i1 = i, k1 = k as Element of L by Def6; ( (id L) . i1 = i1 & (id L) . k1 = k1 ) by FUNCT_1:18; hence (L opp+id) . i >= (L opp+id) . k by A2, A3, ORDERS_2:def_5; ::_thesis: verum end; hence L opp+id is eventually-filtered by WAYBEL_0:12; ::_thesis: verum end; end; definition let L be non empty 1-sorted ; let N be non empty NetStr over L; let i be Element of N; funcN | i -> strict NetStr over L means :Def7: :: WAYBEL_9:def 7 ( ( for x being set holds ( x in the carrier of it iff ex y being Element of N st ( y = x & i <= y ) ) ) & the InternalRel of it = the InternalRel of N |_2 the carrier of it & the mapping of it = the mapping of N | the carrier of it ); existence ex b1 being strict NetStr over L st ( ( for x being set holds ( x in the carrier of b1 iff ex y being Element of N st ( y = x & i <= y ) ) ) & the InternalRel of b1 = the InternalRel of N |_2 the carrier of b1 & the mapping of b1 = the mapping of N | the carrier of b1 ) proof defpred S1[ set ] means ex y being Element of N st ( y = \$1 & i <= y ); consider X being set such that A1: for x being set holds ( x in X iff ( x in the carrier of N & S1[x] ) ) from XBOOLE_0:sch_1(); X c= the carrier of N proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of N ) assume x in X ; ::_thesis: x in the carrier of N hence x in the carrier of N by A1; ::_thesis: verum end; then reconsider f = the mapping of N | X as Function of X, the carrier of L by FUNCT_2:32; set IT = NetStr(# X,( the InternalRel of N |_2 X),f #); take NetStr(# X,( the InternalRel of N |_2 X),f #) ; ::_thesis: ( ( for x being set holds ( x in the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) iff ex y being Element of N st ( y = x & i <= y ) ) ) & the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) ) thus for x being set holds ( x in the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) iff ex y being Element of N st ( y = x & i <= y ) ) by A1; ::_thesis: ( the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) ) thus ( the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict NetStr over L st ( for x being set holds ( x in the carrier of b1 iff ex y being Element of N st ( y = x & i <= y ) ) ) & the InternalRel of b1 = the InternalRel of N |_2 the carrier of b1 & the mapping of b1 = the mapping of N | the carrier of b1 & ( for x being set holds ( x in the carrier of b2 iff ex y being Element of N st ( y = x & i <= y ) ) ) & the InternalRel of b2 = the InternalRel of N |_2 the carrier of b2 & the mapping of b2 = the mapping of N | the carrier of b2 holds b1 = b2 proof defpred S1[ set ] means ex y being Element of N st ( y = \$1 & i <= y ); let A, B be strict NetStr over L; ::_thesis: ( ( for x being set holds ( x in the carrier of A iff ex y being Element of N st ( y = x & i <= y ) ) ) & the InternalRel of A = the InternalRel of N |_2 the carrier of A & the mapping of A = the mapping of N | the carrier of A & ( for x being set holds ( x in the carrier of B iff ex y being Element of N st ( y = x & i <= y ) ) ) & the InternalRel of B = the InternalRel of N |_2 the carrier of B & the mapping of B = the mapping of N | the carrier of B implies A = B ) assume that A2: for x being set holds ( x in the carrier of A iff S1[x] ) and A3: ( the InternalRel of A = the InternalRel of N |_2 the carrier of A & the mapping of A = the mapping of N | the carrier of A ) and A4: for x being set holds ( x in the carrier of B iff S1[x] ) and A5: ( the InternalRel of B = the InternalRel of N |_2 the carrier of B & the mapping of B = the mapping of N | the carrier of B ) ; ::_thesis: A = B the carrier of A = the carrier of B from XBOOLE_0:sch_2(A2, A4); hence A = B by A3, A5; ::_thesis: verum end; end; :: deftheorem Def7 defines | WAYBEL_9:def_7_:_ for L being non empty 1-sorted for N being non empty NetStr over L for i being Element of N for b4 being strict NetStr over L holds ( b4 = N | i iff ( ( for x being set holds ( x in the carrier of b4 iff ex y being Element of N st ( y = x & i <= y ) ) ) & the InternalRel of b4 = the InternalRel of N |_2 the carrier of b4 & the mapping of b4 = the mapping of N | the carrier of b4 ) ); theorem :: WAYBEL_9:12 for L being non empty 1-sorted for N being non empty NetStr over L for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y } proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y } let N be non empty NetStr over L; ::_thesis: for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y } let i be Element of N; ::_thesis: the carrier of (N | i) = { y where y is Element of N : i <= y } thus the carrier of (N | i) c= { y where y is Element of N : i <= y } :: according to XBOOLE_0:def_10 ::_thesis: { y where y is Element of N : i <= y } c= the carrier of (N | i) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the carrier of (N | i) or q in { y where y is Element of N : i <= y } ) assume q in the carrier of (N | i) ; ::_thesis: q in { y where y is Element of N : i <= y } then ex y being Element of N st ( y = q & i <= y ) by Def7; hence q in { y where y is Element of N : i <= y } ; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { y where y is Element of N : i <= y } or q in the carrier of (N | i) ) assume q in { y where y is Element of N : i <= y } ; ::_thesis: q in the carrier of (N | i) then ex y being Element of N st ( q = y & i <= y ) ; hence q in the carrier of (N | i) by Def7; ::_thesis: verum end; theorem Th13: :: WAYBEL_9:13 for L being non empty 1-sorted for N being non empty NetStr over L for i being Element of N holds the carrier of (N | i) c= the carrier of N proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L for i being Element of N holds the carrier of (N | i) c= the carrier of N let N be non empty NetStr over L; ::_thesis: for i being Element of N holds the carrier of (N | i) c= the carrier of N let i be Element of N; ::_thesis: the carrier of (N | i) c= the carrier of N let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (N | i) or x in the carrier of N ) assume x in the carrier of (N | i) ; ::_thesis: x in the carrier of N then ex y being Element of N st ( y = x & i <= y ) by Def7; hence x in the carrier of N ; ::_thesis: verum end; theorem Th14: :: WAYBEL_9:14 for L being non empty 1-sorted for N being non empty NetStr over L for i being Element of N holds N | i is full SubNetStr of N proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L for i being Element of N holds N | i is full SubNetStr of N let N be non empty NetStr over L; ::_thesis: for i being Element of N holds N | i is full SubNetStr of N let i be Element of N; ::_thesis: N | i is full SubNetStr of N A1: the mapping of (N | i) = the mapping of N | the carrier of (N | i) by Def7; the InternalRel of (N | i) = the InternalRel of N |_2 the carrier of (N | i) by Def7; then A2: the InternalRel of (N | i) c= the InternalRel of N by XBOOLE_1:17; the carrier of (N | i) c= the carrier of N by Th13; then N | i is SubRelStr of N by A2, YELLOW_0:def_13; then reconsider K = N | i as SubNetStr of N by A1, YELLOW_6:def_6; the InternalRel of K = the InternalRel of N |_2 the carrier of K by Def7; then K is full SubRelStr of N by YELLOW_0:def_14, YELLOW_6:def_6; hence N | i is full SubNetStr of N by YELLOW_6:def_7; ::_thesis: verum end; registration let L be non empty 1-sorted ; let N be non empty reflexive NetStr over L; let i be Element of N; clusterN | i -> non empty reflexive strict ; coherence ( not N | i is empty & N | i is reflexive ) proof A1: i <= i ; hence not N | i is empty by Def7; ::_thesis: N | i is reflexive reconsider A = N | i as non empty strict NetStr over L by A1, Def7; A is reflexive proof let x be Element of A; :: according to YELLOW_0:def_1 ::_thesis: x <= x consider y being Element of N such that A2: y = x and i <= y by Def7; ( N | i is full SubNetStr of N & y <= y ) by Th14; hence x <= x by A2, YELLOW_6:12; ::_thesis: verum end; hence N | i is reflexive ; ::_thesis: verum end; end; registration let L be non empty 1-sorted ; let N be non empty directed NetStr over L; let i be Element of N; clusterN | i -> non empty strict ; coherence not N | i is empty proof ex z1 being Element of N st ( i <= z1 & i <= z1 ) by YELLOW_6:def_3; hence not N | i is empty by Def7; ::_thesis: verum end; end; registration let L be non empty 1-sorted ; let N be non empty reflexive antisymmetric NetStr over L; let i be Element of N; clusterN | i -> antisymmetric strict ; coherence N | i is antisymmetric proof let x, y be Element of (N | i); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y ) assume A1: ( x <= y & y <= x ) ; ::_thesis: x = y consider y1 being Element of N such that A2: y1 = y and i <= y1 by Def7; consider x1 being Element of N such that A3: x1 = x and i <= x1 by Def7; N | i is SubNetStr of N by Th14; then ( x1 <= y1 & y1 <= x1 ) by A1, A3, A2, YELLOW_6:11; hence x = y by A3, A2, YELLOW_0:def_3; ::_thesis: verum end; end; registration let L be non empty 1-sorted ; let N be non empty antisymmetric directed NetStr over L; let i be Element of N; clusterN | i -> antisymmetric strict ; coherence N | i is antisymmetric proof let x, y be Element of (N | i); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y ) assume A1: ( x <= y & y <= x ) ; ::_thesis: x = y consider y1 being Element of N such that A2: y1 = y and i <= y1 by Def7; consider x1 being Element of N such that A3: x1 = x and i <= x1 by Def7; N | i is SubNetStr of N by Th14; then ( x1 <= y1 & y1 <= x1 ) by A1, A3, A2, YELLOW_6:11; hence x = y by A3, A2, YELLOW_0:def_3; ::_thesis: verum end; end; registration let L be non empty 1-sorted ; let N be non empty reflexive transitive NetStr over L; let i be Element of N; clusterN | i -> transitive strict ; coherence N | i is transitive proof let x, y, z be Element of (N | i); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume that A1: x <= y and A2: y <= z ; ::_thesis: x <= z consider z1 being Element of N such that A3: z1 = z and i <= z1 by Def7; consider x1 being Element of N such that A4: x1 = x and i <= x1 by Def7; consider y1 being Element of N such that A5: y1 = y and i <= y1 by Def7; A6: N | i is full SubNetStr of N by Th14; then A7: y1 <= z1 by A2, A5, A3, YELLOW_6:11; x1 <= y1 by A1, A6, A4, A5, YELLOW_6:11; then x1 <= z1 by A7, YELLOW_0:def_2; hence x <= z by A6, A4, A3, YELLOW_6:12; ::_thesis: verum end; end; registration let L be non empty 1-sorted ; let N be net of L; let i be Element of N; clusterN | i -> transitive strict directed ; coherence ( N | i is transitive & N | i is directed ) proof thus N | i is transitive ::_thesis: N | i is directed proof let x, y, z be Element of (N | i); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume that A1: x <= y and A2: y <= z ; ::_thesis: x <= z consider z1 being Element of N such that A3: z1 = z and i <= z1 by Def7; consider x1 being Element of N such that A4: x1 = x and i <= x1 by Def7; consider y1 being Element of N such that A5: y1 = y and i <= y1 by Def7; A6: N | i is full SubNetStr of N by Th14; then A7: y1 <= z1 by A2, A5, A3, YELLOW_6:11; x1 <= y1 by A1, A6, A4, A5, YELLOW_6:11; then x1 <= z1 by A7, YELLOW_0:def_2; hence x <= z by A6, A4, A3, YELLOW_6:12; ::_thesis: verum end; for x, y being Element of (N | i) ex z being Element of (N | i) st ( x <= z & y <= z ) proof let x, y be Element of (N | i); ::_thesis: ex z being Element of (N | i) st ( x <= z & y <= z ) consider x1 being Element of N such that A8: x1 = x and A9: i <= x1 by Def7; consider y1 being Element of N such that A10: y1 = y and i <= y1 by Def7; consider z1 being Element of N such that A11: x1 <= z1 and A12: y1 <= z1 by YELLOW_6:def_3; i <= z1 by A9, A11, YELLOW_0:def_2; then reconsider z = z1 as Element of (N | i) by Def7; take z ; ::_thesis: ( x <= z & y <= z ) N | i is full SubNetStr of N by Th14; hence ( x <= z & y <= z ) by A8, A10, A11, A12, YELLOW_6:12; ::_thesis: verum end; hence N | i is directed by YELLOW_6:def_3; ::_thesis: verum end; end; theorem :: WAYBEL_9:15 for L being non empty 1-sorted for N being non empty reflexive NetStr over L for i, x being Element of N for x1 being Element of (N | i) st x = x1 holds N . x = (N | i) . x1 proof let L be non empty 1-sorted ; ::_thesis: for N being non empty reflexive NetStr over L for i, x being Element of N for x1 being Element of (N | i) st x = x1 holds N . x = (N | i) . x1 let N be non empty reflexive NetStr over L; ::_thesis: for i, x being Element of N for x1 being Element of (N | i) st x = x1 holds N . x = (N | i) . x1 let i, x be Element of N; ::_thesis: for x1 being Element of (N | i) st x = x1 holds N . x = (N | i) . x1 let x1 be Element of (N | i); ::_thesis: ( x = x1 implies N . x = (N | i) . x1 ) assume x = x1 ; ::_thesis: N . x = (N | i) . x1 hence N . x = ( the mapping of N | the carrier of (N | i)) . x1 by FUNCT_1:49 .= (N | i) . x1 by Def7 ; ::_thesis: verum end; theorem Th16: :: WAYBEL_9:16 for L being non empty 1-sorted for N being non empty directed NetStr over L for i, x being Element of N for x1 being Element of (N | i) st x = x1 holds N . x = (N | i) . x1 proof let L be non empty 1-sorted ; ::_thesis: for N being non empty directed NetStr over L for i, x being Element of N for x1 being Element of (N | i) st x = x1 holds N . x = (N | i) . x1 let N be non empty directed NetStr over L; ::_thesis: for i, x being Element of N for x1 being Element of (N | i) st x = x1 holds N . x = (N | i) . x1 let i, x be Element of N; ::_thesis: for x1 being Element of (N | i) st x = x1 holds N . x = (N | i) . x1 let x1 be Element of (N | i); ::_thesis: ( x = x1 implies N . x = (N | i) . x1 ) assume x = x1 ; ::_thesis: N . x = (N | i) . x1 hence N . x = ( the mapping of N | the carrier of (N | i)) . x1 by FUNCT_1:49 .= (N | i) . x1 by Def7 ; ::_thesis: verum end; theorem Th17: :: WAYBEL_9:17 for L being non empty 1-sorted for N being net of L for i being Element of N holds N | i is subnet of N proof let L be non empty 1-sorted ; ::_thesis: for N being net of L for i being Element of N holds N | i is subnet of N let N be net of L; ::_thesis: for i being Element of N holds N | i is subnet of N let i be Element of N; ::_thesis: N | i is subnet of N reconsider A = N | i as net of L ; A1: the carrier of A c= the carrier of N by Th13; A is subnet of N proof reconsider f = id the carrier of A as Function of A,N by A1, FUNCT_2:7; take f ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of A = the mapping of N * f & ( for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st for b3 being Element of the carrier of A holds ( not b2 <= b3 or b1 <= f . b3 ) ) ) for x being set st x in the carrier of A holds the mapping of A . x = ( the mapping of N * f) . x proof let x be set ; ::_thesis: ( x in the carrier of A implies the mapping of A . x = ( the mapping of N * f) . x ) assume A2: x in the carrier of A ; ::_thesis: the mapping of A . x = ( the mapping of N * f) . x thus the mapping of A . x = ( the mapping of N | the carrier of A) . x by Def7 .= the mapping of N . x by A2, FUNCT_1:49 .= the mapping of N . (f . x) by A2, FUNCT_1:18 .= ( the mapping of N * f) . x by A2, FUNCT_2:15 ; ::_thesis: verum end; hence the mapping of A = the mapping of N * f by FUNCT_2:12; ::_thesis: for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st for b3 being Element of the carrier of A holds ( not b2 <= b3 or b1 <= f . b3 ) let m be Element of N; ::_thesis: ex b1 being Element of the carrier of A st for b2 being Element of the carrier of A holds ( not b1 <= b2 or m <= f . b2 ) consider z being Element of N such that A3: i <= z and A4: m <= z by YELLOW_6:def_3; reconsider n = z as Element of A by A3, Def7; take n ; ::_thesis: for b1 being Element of the carrier of A holds ( not n <= b1 or m <= f . b1 ) let p be Element of A; ::_thesis: ( not n <= p or m <= f . p ) assume A5: n <= p ; ::_thesis: m <= f . p p in the carrier of A ; then reconsider p1 = p as Element of N by A1; A is SubNetStr of N by Th14; then z <= p1 by A5, YELLOW_6:11; then m <= p1 by A4, YELLOW_0:def_2; hence m <= f . p by FUNCT_1:18; ::_thesis: verum end; hence N | i is subnet of N ; ::_thesis: verum end; registration let T be non empty 1-sorted ; let N be net of T; cluster non empty transitive strict directed for subnet of N; existence ex b1 being subnet of N st b1 is strict proof set A = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #); A1: RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) #) = RelStr(# the carrier of N, the InternalRel of N #) ; [#] N is directed by WAYBEL_0:def_6; then [#] NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is directed by A1, WAYBEL_0:3; then reconsider A = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) as net of T by A1, WAYBEL_0:def_6, WAYBEL_8:13; A is subnet of N proof reconsider f = id N as Function of A,N ; take f ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of A = the mapping of N * f & ( for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st for b3 being Element of the carrier of A holds ( not b2 <= b3 or b1 <= f . b3 ) ) ) thus the mapping of A = the mapping of N * f by FUNCT_2:17; ::_thesis: for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st for b3 being Element of the carrier of A holds ( not b2 <= b3 or b1 <= f . b3 ) let m be Element of N; ::_thesis: ex b1 being Element of the carrier of A st for b2 being Element of the carrier of A holds ( not b1 <= b2 or m <= f . b2 ) reconsider n = m as Element of A ; take n ; ::_thesis: for b1 being Element of the carrier of A holds ( not n <= b1 or m <= f . b1 ) let p be Element of A; ::_thesis: ( not n <= p or m <= f . p ) assume A2: n <= p ; ::_thesis: m <= f . p p = f . p by FUNCT_1:18; hence m <= f . p by A1, A2, YELLOW_0:1; ::_thesis: verum end; then reconsider A = A as subnet of N ; take A ; ::_thesis: A is strict thus A is strict ; ::_thesis: verum end; end; definition let L be non empty 1-sorted ; let N be net of L; let i be Element of N; :: original: | redefine funcN | i -> strict subnet of N; coherence N | i is strict subnet of N by Th17; end; definition let S be non empty 1-sorted ; let T be 1-sorted ; let f be Function of S,T; let N be NetStr over S; funcf * N -> strict NetStr over T means :Def8: :: WAYBEL_9:def 8 ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = f * the mapping of N ); existence ex b1 being strict NetStr over T st ( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = f * the mapping of N ) proof take NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) = f * the mapping of N ) thus ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) = f * the mapping of N ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict NetStr over T st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = f * the mapping of N & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b2 = f * the mapping of N holds b1 = b2 ; end; :: deftheorem Def8 defines * WAYBEL_9:def_8_:_ for S being non empty 1-sorted for T being 1-sorted for f being Function of S,T for N being NetStr over S for b5 being strict NetStr over T holds ( b5 = f * N iff ( RelStr(# the carrier of b5, the InternalRel of b5 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b5 = f * the mapping of N ) ); registration let S be non empty 1-sorted ; let T be 1-sorted ; let f be Function of S,T; let N be non empty NetStr over S; clusterf * N -> non empty strict ; coherence not f * N is empty proof RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8; hence not f * N is empty ; ::_thesis: verum end; end; registration let S be non empty 1-sorted ; let T be 1-sorted ; let f be Function of S,T; let N be reflexive NetStr over S; clusterf * N -> reflexive strict ; coherence f * N is reflexive proof RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8; hence the InternalRel of (f * N) is_reflexive_in the carrier of (f * N) by ORDERS_2:def_2; :: according to ORDERS_2:def_2 ::_thesis: verum end; end; registration let S be non empty 1-sorted ; let T be 1-sorted ; let f be Function of S,T; let N be antisymmetric NetStr over S; clusterf * N -> antisymmetric strict ; coherence f * N is antisymmetric proof RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8; then the InternalRel of (f * N) is_antisymmetric_in the carrier of (f * N) by ORDERS_2:def_4; hence f * N is antisymmetric by ORDERS_2:def_4; ::_thesis: verum end; end; registration let S be non empty 1-sorted ; let T be 1-sorted ; let f be Function of S,T; let N be transitive NetStr over S; clusterf * N -> transitive strict ; coherence f * N is transitive proof RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8; then the InternalRel of (f * N) is_transitive_in the carrier of (f * N) by ORDERS_2:def_3; hence f * N is transitive by ORDERS_2:def_3; ::_thesis: verum end; end; registration let S be non empty 1-sorted ; let T be 1-sorted ; let f be Function of S,T; let N be directed NetStr over S; clusterf * N -> strict directed ; coherence f * N is directed proof ( RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) & [#] N is directed ) by Def8, WAYBEL_0:def_6; hence [#] (f * N) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum end; end; theorem Th18: :: WAYBEL_9:18 for L being non empty RelStr for N being non empty NetStr over L for x being Element of L holds (x "/\") * N = x "/\" N proof let L be non empty RelStr ; ::_thesis: for N being non empty NetStr over L for x being Element of L holds (x "/\") * N = x "/\" N let N be non empty NetStr over L; ::_thesis: for x being Element of L holds (x "/\") * N = x "/\" N let x be Element of L; ::_thesis: (x "/\") * N = x "/\" N set n = the mapping of N; A1: RelStr(# the carrier of ((x "/\") * N), the InternalRel of ((x "/\") * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def8 .= RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3 ; A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3; then reconsider f2 = the mapping of (x "/\" N) as Function of the carrier of N, the carrier of L ; A3: for c being Element of N holds ((x "/\") * the mapping of N) . c = f2 . c proof let c be Element of N; ::_thesis: ((x "/\") * the mapping of N) . c = f2 . c consider y being Element of L such that A4: y = the mapping of N . c and A5: f2 . c = x "/\" y by A2, WAYBEL_2:def_3; thus ((x "/\") * the mapping of N) . c = (x "/\") . y by A4, FUNCT_2:15 .= f2 . c by A5, WAYBEL_1:def_18 ; ::_thesis: verum end; the mapping of ((x "/\") * N) = (x "/\") * the mapping of N by Def8 .= the mapping of (x "/\" N) by A3, FUNCT_2:63 ; hence (x "/\") * N = x "/\" N by A1; ::_thesis: verum end; begin theorem :: WAYBEL_9:19 for S, T being TopStruct for F being Subset-Family of S for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds G is open proof let S, T be TopStruct ; ::_thesis: for F being Subset-Family of S for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds G is open let F be Subset-Family of S; ::_thesis: for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds G is open let G be Subset-Family of T; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open implies G is open ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: ( F = G & F is open ) ; ::_thesis: G is open let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in G or P is open ) assume A3: P in G ; ::_thesis: P is open reconsider R = P as Subset of S by A1; R is open by A2, A3, TOPS_2:def_1; hence P in the topology of T by A1, PRE_TOPC:def_2; :: according to PRE_TOPC:def_2 ::_thesis: verum end; theorem :: WAYBEL_9:20 for S, T being TopStruct for F being Subset-Family of S for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds G is closed proof let S, T be TopStruct ; ::_thesis: for F being Subset-Family of S for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds G is closed let F be Subset-Family of S; ::_thesis: for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds G is closed let G be Subset-Family of T; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed implies G is closed ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: ( F = G & F is closed ) ; ::_thesis: G is closed let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not P in G or P is closed ) assume A3: P in G ; ::_thesis: P is closed reconsider R = P as Subset of S by A1; R is closed by A2, A3, TOPS_2:def_2; then ([#] S) \ R is open by PRE_TOPC:def_3; hence ([#] T) \ P in the topology of T by A1, PRE_TOPC:def_2; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: verum end; definition attrc1 is strict ; struct TopRelStr -> TopStruct , RelStr ; aggrTopRelStr(# carrier, InternalRel, topology #) -> TopRelStr ; end; registration let A be non empty set ; let R be Relation of A,A; let T be Subset-Family of A; cluster TopRelStr(# A,R,T #) -> non empty ; coherence not TopRelStr(# A,R,T #) is empty ; end; registration let x be set ; let R be Relation of {x}; let T be Subset-Family of {x}; cluster TopRelStr(# {x},R,T #) -> 1 -element ; coherence TopRelStr(# {x},R,T #) is 1 -element proof thus the carrier of TopRelStr(# {x},R,T #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; registration let X be set ; let O be Order of X; let T be Subset-Family of X; cluster TopRelStr(# X,O,T #) -> reflexive transitive antisymmetric ; coherence ( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric ) proof set A = TopRelStr(# X,O,T #); A1: field the InternalRel of TopRelStr(# X,O,T #) = the carrier of TopRelStr(# X,O,T #) by ORDERS_1:12; then A2: the InternalRel of TopRelStr(# X,O,T #) is_antisymmetric_in the carrier of TopRelStr(# X,O,T #) by RELAT_2:def_12; ( the InternalRel of TopRelStr(# X,O,T #) is_reflexive_in the carrier of TopRelStr(# X,O,T #) & the InternalRel of TopRelStr(# X,O,T #) is_transitive_in the carrier of TopRelStr(# X,O,T #) ) by A1, RELAT_2:def_9, RELAT_2:def_16; hence ( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric ) by A2, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum end; end; Lm4: for tau being Subset-Family of {0} for r being Relation of {0} st tau = {{},{0}} & r = {[0,0]} holds ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) proof let tau be Subset-Family of {0}; ::_thesis: for r being Relation of {0} st tau = {{},{0}} & r = {[0,0]} holds ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) let r be Relation of {0}; ::_thesis: ( tau = {{},{0}} & r = {[0,0]} implies ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) ) assume that A1: tau = {{},{0}} and A2: r = {[0,0]} ; ::_thesis: ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) set T = TopRelStr(# {0},r,tau #); thus TopRelStr(# {0},r,tau #) is reflexive ::_thesis: ( TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) proof let x be Element of TopRelStr(# {0},r,tau #); :: according to YELLOW_0:def_1 ::_thesis: x <= x x = 0 by TARSKI:def_1; then [x,x] in {[0,0]} by TARSKI:def_1; hence x <= x by A2, ORDERS_2:def_5; ::_thesis: verum end; the topology of TopRelStr(# {0},r,tau #) = bool the carrier of TopRelStr(# {0},r,tau #) by A1, ZFMISC_1:24; hence TopRelStr(# {0},r,tau #) is discrete by TDLAT_3:def_1; ::_thesis: ( TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) thus ( TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) ; ::_thesis: verum end; registration cluster finite 1 -element discrete reflexive strict for TopRelStr ; existence ex b1 being TopRelStr st ( b1 is reflexive & b1 is discrete & b1 is strict & b1 is finite & b1 is 1 -element ) proof 0 in {0} by TARSKI:def_1; then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3; {{},{0}} = bool {0} by ZFMISC_1:24; then reconsider tau = {{},{0}} as Subset-Family of {0} ; take TopRelStr(# {0},r,tau #) ; ::_thesis: ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is strict & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) thus ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is strict & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) by Lm4; ::_thesis: verum end; end; definition mode TopLattice is TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr ; end; registration cluster non empty finite 1 -element TopSpace-like Hausdorff discrete reflexive transitive antisymmetric with_suprema with_infima compact strict for TopRelStr ; existence ex b1 being TopLattice st ( b1 is strict & b1 is discrete & b1 is finite & b1 is compact & b1 is Hausdorff & b1 is 1 -element ) proof reconsider C = bool {0} as Subset-Family of {0} ; 0 in {0} by TARSKI:def_1; then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3; {{},{0}} = bool {0} by ZFMISC_1:24; then reconsider A = TopRelStr(# {0},r,C #) as finite 1 -element discrete reflexive TopRelStr by Lm4; reconsider A = A as TopLattice ; take A ; ::_thesis: ( A is strict & A is discrete & A is finite & A is compact & A is Hausdorff & A is 1 -element ) thus ( A is strict & A is discrete & A is finite ) ; ::_thesis: ( A is compact & A is Hausdorff & A is 1 -element ) thus A is compact ; ::_thesis: ( A is Hausdorff & A is 1 -element ) thus A is Hausdorff ::_thesis: A is 1 -element proof let p, q be Point of A; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of K10( the carrier of A) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) assume A1: not p = q ; ::_thesis: ex b1, b2 being Element of K10( the carrier of A) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) p = 0 by TARSKI:def_1; hence ex b1, b2 being Element of K10( the carrier of A) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A1, TARSKI:def_1; ::_thesis: verum end; thus A is 1 -element ; ::_thesis: verum end; end; registration let T be non empty Hausdorff TopSpace; cluster non empty -> non empty Hausdorff for SubSpace of T; coherence for b1 being non empty SubSpace of T holds b1 is Hausdorff ; end; theorem Th21: :: WAYBEL_9:21 for T being non empty TopSpace for p being Point of T for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p proof let T be non empty TopSpace; ::_thesis: for p being Point of T for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p let p be Point of T; ::_thesis: for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p let A be Element of (OpenNeighborhoods p); ::_thesis: A is a_neighborhood of p ex W being Subset of T st ( W = A & p in W & W is open ) by YELLOW_6:29; hence A is a_neighborhood of p by CONNSP_2:3; ::_thesis: verum end; theorem Th22: :: WAYBEL_9:22 for T being non empty TopSpace for p being Point of T for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p) proof let T be non empty TopSpace; ::_thesis: for p being Point of T for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p) let p be Point of T; ::_thesis: for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p) let A, B be Element of (OpenNeighborhoods p); ::_thesis: A /\ B is Element of (OpenNeighborhoods p) consider W being Subset of T such that A1: W = A and A2: ( p in W & W is open ) by YELLOW_6:29; consider X being Subset of T such that A3: X = B and A4: ( p in X & X is open ) by YELLOW_6:29; ( p in A /\ B & W /\ X is open ) by A1, A2, A3, A4, XBOOLE_0:def_4; hence A /\ B is Element of (OpenNeighborhoods p) by A1, A3, YELLOW_6:30; ::_thesis: verum end; theorem :: WAYBEL_9:23 for T being non empty TopSpace for p being Point of T for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p) proof let T be non empty TopSpace; ::_thesis: for p being Point of T for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p) let p be Point of T; ::_thesis: for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p) let A, B be Element of (OpenNeighborhoods p); ::_thesis: A \/ B is Element of (OpenNeighborhoods p) consider W being Subset of T such that A1: W = A and A2: p in W and A3: W is open by YELLOW_6:29; A4: p in A \/ B by A1, A2, XBOOLE_0:def_3; consider X being Subset of T such that A5: X = B and p in X and A6: X is open by YELLOW_6:29; W \/ X is open by A3, A6; hence A \/ B is Element of (OpenNeighborhoods p) by A1, A5, A4, YELLOW_6:30; ::_thesis: verum end; theorem Th24: :: WAYBEL_9:24 for T being non empty TopSpace for p being Element of T for N being net of T st p in Lim N holds for S being Subset of T st S = rng the mapping of N holds p in Cl S proof let T be non empty TopSpace; ::_thesis: for p being Element of T for N being net of T st p in Lim N holds for S being Subset of T st S = rng the mapping of N holds p in Cl S let p be Element of T; ::_thesis: for N being net of T st p in Lim N holds for S being Subset of T st S = rng the mapping of N holds p in Cl S let N be net of T; ::_thesis: ( p in Lim N implies for S being Subset of T st S = rng the mapping of N holds p in Cl S ) assume A1: p in Lim N ; ::_thesis: for S being Subset of T st S = rng the mapping of N holds p in Cl S let S be Subset of T; ::_thesis: ( S = rng the mapping of N implies p in Cl S ) assume S = rng the mapping of N ; ::_thesis: p in Cl S then A2: N is_eventually_in S by Th8; for G being Subset of T st G is open & p in G holds S meets G proof let G be Subset of T; ::_thesis: ( G is open & p in G implies S meets G ) assume that A3: G is open and A4: p in G ; ::_thesis: S meets G G = Int G by A3, TOPS_1:23; then reconsider V = G as a_neighborhood of p by A4, CONNSP_2:def_1; N is_eventually_in V by A1, YELLOW_6:def_15; hence S meets G by A2, YELLOW_6:17; ::_thesis: verum end; hence p in Cl S by PRE_TOPC:def_7; ::_thesis: verum end; theorem Th25: :: WAYBEL_9:25 for T being Hausdorff TopLattice for N being convergent net of T for f being Function of T,T st f is continuous holds f . (lim N) in Lim (f * N) proof let T be Hausdorff TopLattice; ::_thesis: for N being convergent net of T for f being Function of T,T st f is continuous holds f . (lim N) in Lim (f * N) let N be convergent net of T; ::_thesis: for f being Function of T,T st f is continuous holds f . (lim N) in Lim (f * N) let f be Function of T,T; ::_thesis: ( f is continuous implies f . (lim N) in Lim (f * N) ) assume A1: f is continuous ; ::_thesis: f . (lim N) in Lim (f * N) for V being a_neighborhood of f . (lim N) holds f * N is_eventually_in V proof let V be a_neighborhood of f . (lim N); ::_thesis: f * N is_eventually_in V A2: dom f = the carrier of T by FUNCT_2:def_1; consider O being a_neighborhood of lim N such that A3: f .: O c= V by A1, BORSUK_1:def_1; lim N in Lim N by YELLOW_6:def_17; then N is_eventually_in O by YELLOW_6:def_15; then consider s0 being Element of N such that A4: for j being Element of N st s0 <= j holds N . j in O by WAYBEL_0:def_11; A5: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def8; then reconsider s1 = s0 as Element of (f * N) ; take s1 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (f * N) holds ( not s1 <= b1 or (f * N) . b1 in V ) let j1 be Element of (f * N); ::_thesis: ( not s1 <= j1 or (f * N) . j1 in V ) assume A6: s1 <= j1 ; ::_thesis: (f * N) . j1 in V reconsider j = j1 as Element of N by A5; N . j in O by A4, A5, A6, YELLOW_0:1; then A7: f . (N . j) in f .: O by A2, FUNCT_1:def_6; A8: the carrier of (f * N) = dom the mapping of N by A5, FUNCT_2:def_1; (f * N) . j1 = (f * the mapping of N) . j1 by Def8 .= f . (N . j) by A8, FUNCT_1:13 ; hence (f * N) . j1 in V by A3, A7; ::_thesis: verum end; hence f . (lim N) in Lim (f * N) by YELLOW_6:def_15; ::_thesis: verum end; theorem Th26: :: WAYBEL_9:26 for T being Hausdorff TopLattice for N being convergent net of T for x being Element of T st x "/\" is continuous holds x "/\" (lim N) in Lim (x "/\" N) proof let T be Hausdorff TopLattice; ::_thesis: for N being convergent net of T for x being Element of T st x "/\" is continuous holds x "/\" (lim N) in Lim (x "/\" N) let N be convergent net of T; ::_thesis: for x being Element of T st x "/\" is continuous holds x "/\" (lim N) in Lim (x "/\" N) let x be Element of T; ::_thesis: ( x "/\" is continuous implies x "/\" (lim N) in Lim (x "/\" N) ) assume A1: x "/\" is continuous ; ::_thesis: x "/\" (lim N) in Lim (x "/\" N) x "/\" (lim N) = (x "/\") . (lim N) by WAYBEL_1:def_18; then x "/\" (lim N) in Lim ((x "/\") * N) by A1, Th25; hence x "/\" (lim N) in Lim (x "/\" N) by Th18; ::_thesis: verum end; theorem Th27: :: WAYBEL_9:27 for S being Hausdorff TopLattice for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds uparrow x is closed proof let S be Hausdorff TopLattice; ::_thesis: for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds uparrow x is closed let x be Element of S; ::_thesis: ( ( for a being Element of S holds a "/\" is continuous ) implies uparrow x is closed ) assume for a being Element of S holds a "/\" is continuous ; ::_thesis: uparrow x is closed then A1: x "/\" is continuous ; ( (x "/\") " {x} = uparrow x & {x} is closed ) by Th7, PCOMPS_1:7; hence uparrow x is closed by A1, PRE_TOPC:def_6; ::_thesis: verum end; theorem Th28: :: WAYBEL_9:28 for S being Hausdorff compact TopLattice for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds downarrow x is closed proof let S be Hausdorff compact TopLattice; ::_thesis: for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds downarrow x is closed let b be Element of S; ::_thesis: ( ( for b being Element of S holds b "/\" is continuous ) implies downarrow b is closed ) assume for a being Element of S holds a "/\" is continuous ; ::_thesis: downarrow b is closed then A1: b "/\" is continuous ; set g1 = (rng (b "/\")) |` (b "/\"); A2: (rng (b "/\")) |` (b "/\") = b "/\" by RELAT_1:94; A3: dom (b "/\") = the carrier of S by FUNCT_2:def_1; A4: {b} "/\" ([#] S) = { (b "/\" y) where y is Element of S : y in [#] S } by YELLOW_4:42; A5: rng (b "/\") = {b} "/\" ([#] S) proof thus rng (b "/\") c= {b} "/\" ([#] S) :: according to XBOOLE_0:def_10 ::_thesis: {b} "/\" ([#] S) c= rng (b "/\") proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng (b "/\") or q in {b} "/\" ([#] S) ) assume q in rng (b "/\") ; ::_thesis: q in {b} "/\" ([#] S) then consider x being set such that A6: x in dom (b "/\") and A7: (b "/\") . x = q by FUNCT_1:def_3; reconsider x1 = x as Element of S by A6; q = b "/\" x1 by A7, WAYBEL_1:def_18; hence q in {b} "/\" ([#] S) by A4; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {b} "/\" ([#] S) or q in rng (b "/\") ) assume q in {b} "/\" ([#] S) ; ::_thesis: q in rng (b "/\") then consider y being Element of S such that A8: q = b "/\" y and y in [#] S by A4; q = (b "/\") . y by A8, WAYBEL_1:def_18; hence q in rng (b "/\") by A3, FUNCT_1:def_3; ::_thesis: verum end; then rng ((rng (b "/\")) |` (b "/\")) = {b} "/\" ([#] S) by RELAT_1:94 .= [#] (S | (rng (b "/\"))) by A5, PRE_TOPC:def_5 .= the carrier of (S | (rng (b "/\"))) ; then reconsider g1 = (rng (b "/\")) |` (b "/\") as Function of S,(S | (rng (b "/\"))) by A2, A3, FUNCT_2:1; rng g1 = {b} "/\" ([#] S) by A5, RELAT_1:94 .= [#] (S | ({b} "/\" ([#] S))) by PRE_TOPC:def_5 ; then S | ({b} "/\" ([#] S)) is compact by A1, A2, A5, COMPTS_1:14, PRE_TOPC:27; then {b} "/\" ([#] S) is compact by COMPTS_1:3; hence downarrow b is closed by Th5; ::_thesis: verum end; begin definition let T be non empty TopSpace; let N be non empty NetStr over T; let p be Point of T; predp is_a_cluster_point_of N means :Def9: :: WAYBEL_9:def 9 for O being a_neighborhood of p holds N is_often_in O; end; :: deftheorem Def9 defines is_a_cluster_point_of WAYBEL_9:def_9_:_ for T being non empty TopSpace for N being non empty NetStr over T for p being Point of T holds ( p is_a_cluster_point_of N iff for O being a_neighborhood of p holds N is_often_in O ); theorem :: WAYBEL_9:29 for L being non empty TopSpace for N being net of L for c being Point of L st c in Lim N holds c is_a_cluster_point_of N proof let L be non empty TopSpace; ::_thesis: for N being net of L for c being Point of L st c in Lim N holds c is_a_cluster_point_of N let N be net of L; ::_thesis: for c being Point of L st c in Lim N holds c is_a_cluster_point_of N let c be Point of L; ::_thesis: ( c in Lim N implies c is_a_cluster_point_of N ) assume A1: c in Lim N ; ::_thesis: c is_a_cluster_point_of N let O be a_neighborhood of c; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in O N is_eventually_in O by A1, YELLOW_6:def_15; hence N is_often_in O by YELLOW_6:19; ::_thesis: verum end; theorem Th30: :: WAYBEL_9:30 for T being non empty Hausdorff compact TopSpace for N being net of T ex c being Point of T st c is_a_cluster_point_of N proof let T be non empty Hausdorff compact TopSpace; ::_thesis: for N being net of T ex c being Point of T st c is_a_cluster_point_of N let N be net of T; ::_thesis: ex c being Point of T st c is_a_cluster_point_of N defpred S1[ set , set ] means ex X being Subset of T ex a being Element of N st ( a = \$1 & X = { (N . j) where j is Element of N : a <= j } & \$2 = Cl X ); A1: for e being Element of N ex u being Subset of T st S1[e,u] proof let e be Element of N; ::_thesis: ex u being Subset of T st S1[e,u] reconsider a = e as Element of N ; { (N . j) where j is Element of N : a <= j } c= the carrier of T proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (N . j) where j is Element of N : a <= j } or q in the carrier of T ) assume q in { (N . j) where j is Element of N : a <= j } ; ::_thesis: q in the carrier of T then ex j being Element of N st ( q = N . j & a <= j ) ; hence q in the carrier of T ; ::_thesis: verum end; then reconsider X = { (N . j) where j is Element of N : a <= j } as Subset of the carrier of T ; take Cl X ; ::_thesis: S1[e, Cl X] take X ; ::_thesis: ex a being Element of N st ( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X ) take a ; ::_thesis: ( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X ) thus ( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X ) ; ::_thesis: verum end; consider F being Function of the carrier of N,(bool the carrier of T) such that A2: for e being Element of N holds S1[e,F . e] from FUNCT_2:sch_3(A1); reconsider RF = rng F as Subset-Family of T ; A3: dom F = the carrier of N by FUNCT_2:def_1; A4: RF is centered proof thus RF <> {} by A3, RELAT_1:42; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds ( b1 = {} or not b1 c= RF or not b1 is finite or not meet b1 = {} ) defpred S2[ set , set ] means ex i being Element of N ex h, Ch being Subset of T st ( i = \$2 & Ch = \$1 & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ); set J = { i where i is Element of N : ex h, Ch being Subset of T st ( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } ; let H be set ; ::_thesis: ( H = {} or not H c= RF or not H is finite or not meet H = {} ) assume that A5: H <> {} and A6: H c= RF and A7: H is finite ; ::_thesis: not meet H = {} reconsider H1 = H as non empty set by A5; set e = the Element of H1; the Element of H1 in RF by A6, TARSKI:def_3; then consider x being set such that A8: x in dom F and the Element of H1 = F . x by FUNCT_1:def_3; reconsider x = x as Element of N by A8; consider X being Subset of T, a being Element of N such that a = x and A9: ( X = { (N . j) where j is Element of N : a <= j } & F . x = Cl X ) by A2; a in { i where i is Element of N : ex h, Ch being Subset of T st ( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } by A9; then reconsider J = { i where i is Element of N : ex h, Ch being Subset of T st ( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } as non empty set ; A10: for e being Element of H1 ex u being Element of J st S2[e,u] proof let e be Element of H1; ::_thesis: ex u being Element of J st S2[e,u] e in RF by A6, TARSKI:def_3; then consider x being set such that A11: x in dom F and A12: e = F . x by FUNCT_1:def_3; reconsider x = x as Element of N by A11; consider X being Subset of T, a being Element of N such that A13: a = x and A14: X = { (N . j) where j is Element of N : a <= j } and A15: F . x = Cl X by A2; a in J by A14, A15; then reconsider a = a as Element of J ; take u = a; ::_thesis: S2[e,u] take i = x; ::_thesis: ex h, Ch being Subset of T st ( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) take h = X; ::_thesis: ex Ch being Subset of T st ( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) take Ch = Cl X; ::_thesis: ( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) thus i = u by A13; ::_thesis: ( Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) thus Ch = e by A12, A15; ::_thesis: ( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) thus h = { (N . j) where j is Element of N : i <= j } by A13, A14; ::_thesis: Ch = Cl h thus Ch = Cl h ; ::_thesis: verum end; consider Q being Function of H1,J such that A16: for e being Element of H1 holds S2[e,Q . e] from FUNCT_2:sch_3(A10); rng Q c= [#] N proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng Q or q in [#] N ) assume q in rng Q ; ::_thesis: q in [#] N then consider x being set such that A17: x in dom Q and A18: Q . x = q by FUNCT_1:def_3; reconsider x = x as Element of H1 by A17; ex i being Element of N ex h, Ch being Subset of T st ( i = Q . x & Ch = x & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) by A16; hence q in [#] N by A18; ::_thesis: verum end; then reconsider RQ = rng Q as Subset of ([#] N) ; A19: ( not [#] N is empty & [#] N is directed ) by WAYBEL_0:def_6; dom Q = H by FUNCT_2:def_1; then rng Q is finite by A7, FINSET_1:8; then consider i0 being Element of N such that i0 in [#] N and A20: i0 is_>=_than RQ by A19, WAYBEL_0:1; for Y being set st Y in H holds N . i0 in Y proof let Y be set ; ::_thesis: ( Y in H implies N . i0 in Y ) assume A21: Y in H ; ::_thesis: N . i0 in Y then consider i being Element of N, h, Ch being Subset of T such that A22: i = Q . Y and A23: Ch = Y and A24: h = { (N . j) where j is Element of N : i <= j } and A25: Ch = Cl h by A16; Y in dom Q by A21, FUNCT_2:def_1; then i in rng Q by A22, FUNCT_1:def_3; then i <= i0 by A20, LATTICE3:def_9; then A26: N . i0 in h by A24; h c= Cl h by PRE_TOPC:18; hence N . i0 in Y by A23, A25, A26; ::_thesis: verum end; hence not meet H = {} by A5, SETFAM_1:def_1; ::_thesis: verum end; RF is closed proof let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not P in RF or P is closed ) assume P in RF ; ::_thesis: P is closed then consider x being set such that A27: x in dom F and A28: F . x = P by FUNCT_1:def_3; reconsider x = x as Element of N by A27; ex X being Subset of T ex a being Element of N st ( a = x & X = { (N . j) where j is Element of N : a <= j } & F . x = Cl X ) by A2; then P = Cl P by A28; hence P is closed ; ::_thesis: verum end; then meet RF <> {} by A4, COMPTS_1:4; then consider c being set such that A29: c in meet RF by XBOOLE_0:def_1; reconsider c = c as Point of T by A29; take c ; ::_thesis: c is_a_cluster_point_of N assume not c is_a_cluster_point_of N ; ::_thesis: contradiction then consider O being a_neighborhood of c such that A30: not N is_often_in O by Def9; N is_eventually_in the carrier of T \ O by A30, WAYBEL_0:10; then consider s0 being Element of N such that A31: for j being Element of N st s0 <= j holds N . j in the carrier of T \ O by WAYBEL_0:def_11; consider Y being Subset of T, a being Element of N such that A32: ( a = s0 & Y = { (N . j) where j is Element of N : a <= j } ) and A33: F . s0 = Cl Y by A2; Cl Y in RF by A3, A33, FUNCT_1:def_3; then A34: c in Cl Y by A29, SETFAM_1:def_1; {} = O /\ Y proof thus {} c= O /\ Y by XBOOLE_1:2; :: according to XBOOLE_0:def_10 ::_thesis: O /\ Y c= {} let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in O /\ Y or q in {} ) assume A35: q in O /\ Y ; ::_thesis: q in {} q in Y by A35, XBOOLE_0:def_4; then consider j being Element of N such that A36: q = N . j and A37: s0 <= j by A32; assume not q in {} ; ::_thesis: contradiction N . j in the carrier of T \ O by A31, A37; then not N . j in O by XBOOLE_0:def_5; hence contradiction by A35, A36, XBOOLE_0:def_4; ::_thesis: verum end; then O misses Y by XBOOLE_0:def_7; then A38: Int O misses Y by TOPS_1:16, XBOOLE_1:63; ( Int O is open & c in Int O ) by CONNSP_2:def_1; hence contradiction by A34, A38, PRE_TOPC:def_7; ::_thesis: verum end; theorem Th31: :: WAYBEL_9:31 for L being non empty TopSpace for N being net of L for M being subnet of N for c being Point of L st c is_a_cluster_point_of M holds c is_a_cluster_point_of N proof let L be non empty TopSpace; ::_thesis: for N being net of L for M being subnet of N for c being Point of L st c is_a_cluster_point_of M holds c is_a_cluster_point_of N let N be net of L; ::_thesis: for M being subnet of N for c being Point of L st c is_a_cluster_point_of M holds c is_a_cluster_point_of N let M be subnet of N; ::_thesis: for c being Point of L st c is_a_cluster_point_of M holds c is_a_cluster_point_of N let c be Point of L; ::_thesis: ( c is_a_cluster_point_of M implies c is_a_cluster_point_of N ) assume A1: c is_a_cluster_point_of M ; ::_thesis: c is_a_cluster_point_of N let O be a_neighborhood of c; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in O M is_often_in O by A1, Def9; hence N is_often_in O by YELLOW_6:18; ::_thesis: verum end; theorem Th32: :: WAYBEL_9:32 for T being non empty TopSpace for N being net of T for x being Point of T st x is_a_cluster_point_of N holds ex M being subnet of N st x in Lim M proof let T be non empty TopSpace; ::_thesis: for N being net of T for x being Point of T st x is_a_cluster_point_of N holds ex M being subnet of N st x in Lim M let N be net of T; ::_thesis: for x being Point of T st x is_a_cluster_point_of N holds ex M being subnet of N st x in Lim M let x be Point of T; ::_thesis: ( x is_a_cluster_point_of N implies ex M being subnet of N st x in Lim M ) assume A1: x is_a_cluster_point_of N ; ::_thesis: ex M being subnet of N st x in Lim M set q = the Element of N; set S9 = { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O } ; reconsider O = [#] T as Element of (OpenNeighborhoods x) by YELLOW_6:30; N . the Element of N in [#] T ; then [ the Element of N,O] in { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O } ; then reconsider S9 = { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O } as non empty set ; set n = the mapping of N; defpred S1[ set , set ] means ex s1, s2 being Element of N st ( s1 = \$1 `1 & s2 = \$2 `1 & s1 <= s2 & \$2 `2 c= \$1 `2 ); consider L being non empty strict RelStr such that A2: the carrier of L = S9 and A3: for a, b being Element of L holds ( a <= b iff S1[a,b] ) from YELLOW_0:sch_1(); deffunc H1( Element of L) -> set = the mapping of N . (\$1 `1); A4: for a being Element of L holds H1(a) in the carrier of T proof let a be Element of L; ::_thesis: H1(a) in the carrier of T a in S9 by A2; then consider s being Element of N, O being Element of (OpenNeighborhoods x) such that A5: a = [s,O] and N . s in O ; the mapping of N . (a `1) = the mapping of N . s by A5, MCART_1:7; hence H1(a) in the carrier of T ; ::_thesis: verum end; consider g being Function of the carrier of L, the carrier of T such that A6: for x being Element of L holds g . x = H1(x) from FUNCT_2:sch_8(A4); set M = NetStr(# the carrier of L, the InternalRel of L,g #); for a, b being Element of NetStr(# the carrier of L, the InternalRel of L,g #) ex z being Element of NetStr(# the carrier of L, the InternalRel of L,g #) st ( a <= z & b <= z ) proof let a, b be Element of NetStr(# the carrier of L, the InternalRel of L,g #); ::_thesis: ex z being Element of NetStr(# the carrier of L, the InternalRel of L,g #) st ( a <= z & b <= z ) a in S9 by A2; then consider aa being Element of N, Oa being Element of (OpenNeighborhoods x) such that A7: a = [aa,Oa] and N . aa in Oa ; b in S9 by A2; then consider bb being Element of N, Ob being Element of (OpenNeighborhoods x) such that A8: b = [bb,Ob] and N . bb in Ob ; consider z1 being Element of N such that A9: aa <= z1 and A10: bb <= z1 by YELLOW_6:def_3; ( Oa is a_neighborhood of x & Ob is a_neighborhood of x ) by Th21; then Oa /\ Ob is a_neighborhood of x by CONNSP_2:2; then N is_often_in Oa /\ Ob by A1, Def9; then consider d being Element of N such that A11: z1 <= d and A12: N . d in Oa /\ Ob by WAYBEL_0:def_12; Oa /\ Ob is Element of (OpenNeighborhoods x) by Th22; then [d,(Oa /\ Ob)] in S9 by A12; then reconsider z = [d,(Oa /\ Ob)] as Element of NetStr(# the carrier of L, the InternalRel of L,g #) by A2; reconsider A1 = a, C7 = b, z2 = z as Element of L ; A13: ( C7 `1 = bb & C7 `2 = Ob ) by A8, MCART_1:7; take z ; ::_thesis: ( a <= z & b <= z ) A14: ( A1 `1 = aa & A1 `2 = Oa ) by A7, MCART_1:7; A15: ( z2 `1 = d & z2 `2 = Oa /\ Ob ) by MCART_1:7; ( Oa /\ Ob c= Ob & bb <= d ) by A10, A11, XBOOLE_1:17, YELLOW_0:def_2; then A16: C7 <= z2 by A3, A13, A15; ( Oa /\ Ob c= Oa & aa <= d ) by A9, A11, XBOOLE_1:17, YELLOW_0:def_2; then A1 <= z2 by A3, A14, A15; hence ( a <= z & b <= z ) by A16, YELLOW_0:1; ::_thesis: verum end; then reconsider M = NetStr(# the carrier of L, the InternalRel of L,g #) as prenet of T by YELLOW_6:def_3; M is transitive proof let x, y, z be Element of M; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume that A17: x <= y and A18: y <= z ; ::_thesis: x <= z reconsider x1 = x, y1 = y, z1 = z as Element of L ; x1 <= y1 by A17, YELLOW_0:1; then consider sx, sy being Element of N such that A19: sx = x1 `1 and A20: ( sy = y1 `1 & sx <= sy & y1 `2 c= x1 `2 ) by A3; y1 <= z1 by A18, YELLOW_0:1; then consider s1, s2 being Element of N such that A21: s1 = y1 `1 and A22: s2 = z1 `1 and A23: ( s1 <= s2 & z1 `2 c= y1 `2 ) by A3; ( sx <= s2 & z1 `2 c= x1 `2 ) by A20, A21, A23, XBOOLE_1:1, YELLOW_0:def_2; then x1 <= z1 by A3, A19, A22; hence x <= z by YELLOW_0:1; ::_thesis: verum end; then reconsider M = M as net of T ; M is subnet of N proof deffunc H2( Element of L) -> set = \$1 `1 ; A24: for a being Element of L holds H2(a) in the carrier of N proof let a be Element of L; ::_thesis: H2(a) in the carrier of N a in S9 by A2; then consider s being Element of N, O being Element of (OpenNeighborhoods x) such that A25: a = [s,O] and N . s in O ; a `1 = s by A25, MCART_1:7; hence H2(a) in the carrier of N ; ::_thesis: verum end; consider f being Function of the carrier of L, the carrier of N such that A26: for x being Element of L holds f . x = H2(x) from FUNCT_2:sch_8(A24); reconsider f = f as Function of M,N ; take f ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of M = the mapping of N * f & ( for b1 being Element of the carrier of N ex b2 being Element of the carrier of M st for b3 being Element of the carrier of M holds ( not b2 <= b3 or b1 <= f . b3 ) ) ) for x being set st x in the carrier of M holds g . x = ( the mapping of N * f) . x proof let x be set ; ::_thesis: ( x in the carrier of M implies g . x = ( the mapping of N * f) . x ) assume A27: x in the carrier of M ; ::_thesis: g . x = ( the mapping of N * f) . x hence g . x = the mapping of N . (x `1) by A6 .= the mapping of N . (f . x) by A26, A27 .= ( the mapping of N * f) . x by A27, FUNCT_2:15 ; ::_thesis: verum end; hence the mapping of M = the mapping of N * f by FUNCT_2:12; ::_thesis: for b1 being Element of the carrier of N ex b2 being Element of the carrier of M st for b3 being Element of the carrier of M holds ( not b2 <= b3 or b1 <= f . b3 ) let m be Element of N; ::_thesis: ex b1 being Element of the carrier of M st for b2 being Element of the carrier of M holds ( not b1 <= b2 or m <= f . b2 ) N . m in [#] T ; then [m,O] in S9 ; then reconsider n = [m,O] as Element of M by A2; take n ; ::_thesis: for b1 being Element of the carrier of M holds ( not n <= b1 or m <= f . b1 ) let p be Element of M; ::_thesis: ( not n <= p or m <= f . p ) assume A28: n <= p ; ::_thesis: m <= f . p reconsider n1 = n, p1 = p as Element of L ; n1 <= p1 by A28, YELLOW_0:1; then A29: ex s1, s2 being Element of N st ( s1 = n1 `1 & s2 = p1 `1 & s1 <= s2 & p1 `2 c= n1 `2 ) by A3; f . p = p `1 by A26; hence m <= f . p by A29, MCART_1:7; ::_thesis: verum end; then reconsider M = M as subnet of N ; take M ; ::_thesis: x in Lim M for V being a_neighborhood of x holds M is_eventually_in V proof set i = the Element of N; let V be a_neighborhood of x; ::_thesis: M is_eventually_in V ( x in Int V & Int V is open ) by CONNSP_2:def_1; then A30: Int V in the carrier of (OpenNeighborhoods x) by YELLOW_6:30; then Int V is a_neighborhood of x by Th21; then N is_often_in Int V by A1, Def9; then consider s being Element of N such that the Element of N <= s and A31: N . s in Int V by WAYBEL_0:def_12; A32: M is_eventually_in Int V proof [s,(Int V)] in S9 by A30, A31; then reconsider j = [s,(Int V)] as Element of M by A2; take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of M holds ( not j <= b1 or M . b1 in Int V ) let s9 be Element of M; ::_thesis: ( not j <= s9 or M . s9 in Int V ) assume A33: j <= s9 ; ::_thesis: M . s9 in Int V reconsider j1 = j, s1 = s9 as Element of L ; j1 <= s1 by A33, YELLOW_0:1; then A34: ex s1, s2 being Element of N st ( s1 = j `1 & s2 = s9 `1 & s1 <= s2 & s9 `2 c= j `2 ) by A3; s9 in S9 by A2; then consider ss being Element of N, OO being Element of (OpenNeighborhoods x) such that A35: s9 = [ss,OO] and A36: N . ss in OO ; A37: ( j `2 = Int V & s9 `2 = OO ) by A35, MCART_1:7; M . s9 = the mapping of N . (s9 `1) by A6 .= N . ss by A35, MCART_1:7 ; hence M . s9 in Int V by A36, A34, A37; ::_thesis: verum end; Int V c= V by TOPS_1:16; hence M is_eventually_in V by A32, WAYBEL_0:8; ::_thesis: verum end; hence x in Lim M by YELLOW_6:def_15; ::_thesis: verum end; theorem Th33: :: WAYBEL_9:33 for L being non empty Hausdorff compact TopSpace for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d ) holds for s being Point of L st s is_a_cluster_point_of N holds s in Lim N proof let L be non empty Hausdorff compact TopSpace; ::_thesis: for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d ) holds for s being Point of L st s is_a_cluster_point_of N holds s in Lim N let N be net of L; ::_thesis: ( ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d ) implies for s being Point of L st s is_a_cluster_point_of N holds s in Lim N ) assume A1: for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d ; ::_thesis: for s being Point of L st s is_a_cluster_point_of N holds s in Lim N let c be Point of L; ::_thesis: ( c is_a_cluster_point_of N implies c in Lim N ) assume A2: c is_a_cluster_point_of N ; ::_thesis: c in Lim N assume not c in Lim N ; ::_thesis: contradiction then consider M being subnet of N such that A3: for P being subnet of M holds not c in Lim P by YELLOW_6:37; consider d being Point of L such that A4: d is_a_cluster_point_of M by Th30; A5: d is_a_cluster_point_of N by A4, Th31; c <> d by A3, A4, Th32; hence contradiction by A1, A2, A5; ::_thesis: verum end; theorem Th34: :: WAYBEL_9:34 for S being non empty TopSpace for c being Point of S for N being net of S for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds c in A proof let S be non empty TopSpace; ::_thesis: for c being Point of S for N being net of S for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds c in A let c be Point of S; ::_thesis: for N being net of S for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds c in A let N be net of S; ::_thesis: for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds c in A let A be Subset of S; ::_thesis: ( c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A implies c in A ) assume that A1: c is_a_cluster_point_of N and A2: A is closed and A3: rng the mapping of N c= A ; ::_thesis: c in A consider M being subnet of N such that A4: c in Lim M by A1, Th32; reconsider R = rng the mapping of M as Subset of S ; ex f being Function of M,N st ( the mapping of M = the mapping of N * f & ( for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= f . p ) ) by YELLOW_6:def_9; then R c= rng the mapping of N by RELAT_1:26; then R c= A by A3, XBOOLE_1:1; then A5: Cl R c= Cl A by PRE_TOPC:19; c in Cl R by A4, Th24; then c in Cl A by A5; hence c in A by A2, PRE_TOPC:22; ::_thesis: verum end; Lm5: for S being Hausdorff compact TopLattice for N being net of S for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds d is_>=_than rng the mapping of N proof let S be Hausdorff compact TopLattice; ::_thesis: for N being net of S for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds d is_>=_than rng the mapping of N let N be net of S; ::_thesis: for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds d is_>=_than rng the mapping of N let c be Point of S; ::_thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds d is_>=_than rng the mapping of N let d be Element of S; ::_thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N implies d is_>=_than rng the mapping of N ) 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: d is_>=_than rng the mapping of N let i be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not i in rng the mapping of N or i <= d ) assume i in rng the mapping of N ; ::_thesis: i <= d 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_3; reconsider i1 = iJ as Element of N by A5; uparrow (N . i1) is closed by A2, Th27; then A7: Cl (uparrow (N . i1)) = uparrow (N . i1) by PRE_TOPC:22; N is_eventually_in uparrow (N . i1) proof consider j being Element of N such that A8: 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: for b1 being Element of the carrier of N holds ( not j <= b1 or N . b1 in uparrow (N . i1) ) let k be Element of N; ::_thesis: ( not j <= k or N . k in uparrow (N . i1) ) assume j <= k ; ::_thesis: N . k in uparrow (N . i1) then N . i1 <= N . k by A8; hence N . k in uparrow (N . i1) by WAYBEL_0:18; ::_thesis: verum end; then consider t being Element of N such that A9: for j being Element of N st t <= j holds N . j in uparrow (N . i1) by WAYBEL_0:def_11; reconsider A = N | t as subnet of N ; A10: rng the mapping of A c= uparrow (N . i1) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng the mapping of A or q in uparrow (N . i1) ) assume q in rng the mapping of A ; ::_thesis: q in uparrow (N . i1) then consider x being set such that A11: x in dom the mapping of A and A12: q = the mapping of A . x by FUNCT_1:def_3; reconsider x = x as Element of A by A11; consider y being Element of N such that A13: y = x and A14: t <= y by Def7; A . x = N . y by A13, Th16; hence q in uparrow (N . i1) by A9, A12, A14; ::_thesis: verum end; c is_a_cluster_point_of A proof let O be a_neighborhood of c; :: according to WAYBEL_9:def_9 ::_thesis: A is_often_in O let i be Element of A; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of A st ( i <= b1 & A . b1 in O ) consider i2 being Element of N such that A15: i2 = i and A16: t <= i2 by Def7; N is_often_in O by A4, Def9; then consider j2 being Element of N such that A17: i2 <= j2 and A18: N . j2 in O by WAYBEL_0:def_12; t <= j2 by A16, A17, YELLOW_0:def_2; then reconsider j = j2 as Element of A by Def7; take j ; ::_thesis: ( i <= j & A . j in O ) A is full SubNetStr of N by Th14; hence i <= j by A15, A17, YELLOW_6:12; ::_thesis: A . j in O thus A . j in O by A18, Th16; ::_thesis: verum end; then consider M being subnet of A such that A19: c in Lim M by Th32; reconsider R = rng the mapping of M as Subset of S ; A20: uparrow (N . i1) = { z where z is Element of S : z "/\" (N . i1) = N . i1 } by Lm1; ex f being Function of M,A st ( the mapping of M = the mapping of A * f & ( 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_9; then R c= rng the mapping of A by RELAT_1:26; then R c= uparrow (N . i1) by A10, XBOOLE_1:1; then A21: Cl R c= Cl (uparrow (N . i1)) by PRE_TOPC:19; c in Cl R by A19, Th24; then c in uparrow (N . i1) by A7, A21; then ex z being Element of S st ( c = z & z "/\" (N . i1) = N . i1 ) by A20; hence i <= d by A1, A6, YELLOW_0:25; ::_thesis: verum end; Lm6: for S being Hausdorff compact TopLattice for N being net of S for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds for b being Element of S st rng the mapping of N is_<=_than b holds d <= b proof let S be Hausdorff compact TopLattice; ::_thesis: for N being net of S for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds for b being Element of S st rng the mapping of N is_<=_than b holds d <= b let N be net of S; ::_thesis: for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds for b being Element of S st rng the mapping of N is_<=_than b holds d <= b let c be Point of S; ::_thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds for b being Element of S st rng the mapping of N is_<=_than b holds d <= b let d be Element of S; ::_thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N implies for b being Element of S st rng the mapping of N is_<=_than b holds d <= b ) assume that A1: c = d and A2: for x being Element of S holds x "/\" is continuous and A3: c is_a_cluster_point_of N ; ::_thesis: for b being Element of S st rng the mapping of N is_<=_than b holds d <= b let b be Element of S; ::_thesis: ( rng the mapping of N is_<=_than b implies d <= b ) assume A4: rng the mapping of N is_<=_than b ; ::_thesis: d <= b A5: now__::_thesis:_for_i_being_Element_of_N_holds_N_._i_in_{b}_"/\"_([#]_S) let i be Element of N; ::_thesis: N . i in {b} "/\" ([#] S) A6: the carrier of N = dom the mapping of N by FUNCT_2:def_1; N . i in rng the mapping of N by A6, FUNCT_1:def_3; then N . i <= b by A4, LATTICE3:def_9; then A7: b "/\" (N . i) = N . i by YELLOW_0:25; b in {b} by TARSKI:def_1; hence N . i in {b} "/\" ([#] S) by A7, YELLOW_4:37; ::_thesis: verum end; A8: rng the mapping of N c= {b} "/\" ([#] S) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng the mapping of N or y in {b} "/\" ([#] S) ) assume y in rng the mapping of N ; ::_thesis: y in {b} "/\" ([#] S) then consider x being set such that A9: x in dom the mapping of N and A10: y = the mapping of N . x by FUNCT_1:def_3; reconsider x = x as Element of N by A9; y = N . x by A10; hence y in {b} "/\" ([#] S) by A5; ::_thesis: verum end; downarrow b is closed by A2, Th28; then {b} "/\" ([#] S) is closed by Th5; then ( {b} "/\" ([#] S) = { (b "/\" y) where y is Element of S : y in [#] S } & c in {b} "/\" ([#] S) ) by A3, A8, Th34, YELLOW_4:42; then ex y being Element of S st ( c = b "/\" y & y in [#] S ) ; hence d <= b by A1, YELLOW_0:23; ::_thesis: verum end; theorem Th35: :: WAYBEL_9:35 for S being Hausdorff compact TopLattice for c being Point of S for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds c = sup N proof let S be Hausdorff compact TopLattice; ::_thesis: for c being Point of S for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds c = sup N let c be Point of S; ::_thesis: for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds c = sup N let N be net of S; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N implies c = sup N ) assume A1: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N ) ; ::_thesis: c = sup N reconsider c9 = c as Element of S ; ( c9 is_>=_than rng the mapping of N & ( for b being Element of S st rng the mapping of N is_<=_than b holds c9 <= b ) ) by A1, Lm5, Lm6; hence c = sup (rng the mapping of N) by YELLOW_0:30 .= sup N by YELLOW_2:def_5 ; ::_thesis: verum end; Lm7: for S being Hausdorff compact TopLattice for N being net of S for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds d is_<=_than rng the mapping of N proof let S be Hausdorff compact TopLattice; ::_thesis: for N being net of S for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds d is_<=_than rng the mapping of N let N be net of S; ::_thesis: for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds d is_<=_than rng the mapping of N let c be Point of S; ::_thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds d is_<=_than rng the mapping of N let d be Element of S; ::_thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N implies d is_<=_than rng the mapping of N ) assume that A1: c = d and A2: for x being Element of S holds x "/\" is continuous and A3: N is eventually-filtered and A4: c is_a_cluster_point_of N ; ::_thesis: d is_<=_than rng the mapping of N let i be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not i in rng the mapping of N or d <= i ) assume i in rng the mapping of N ; ::_thesis: d <= i 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_3; reconsider i1 = iJ as Element of N by A5; downarrow (N . i1) is closed by A2, Th28; then A7: Cl (downarrow (N . i1)) = downarrow (N . i1) by PRE_TOPC:22; N is_eventually_in downarrow (N . i1) proof consider j being Element of N such that A8: for k being Element of N st j <= k holds N . i1 >= N . k by A3, WAYBEL_0:12; take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not j <= b1 or N . b1 in downarrow (N . i1) ) let k be Element of N; ::_thesis: ( not j <= k or N . k in downarrow (N . i1) ) assume j <= k ; ::_thesis: N . k in downarrow (N . i1) then N . i1 >= N . k by A8; hence N . k in downarrow (N . i1) by WAYBEL_0:17; ::_thesis: verum end; then consider t being Element of N such that A9: for j being Element of N st t <= j holds N . j in downarrow (N . i1) by WAYBEL_0:def_11; reconsider A = N | t as subnet of N ; A10: rng the mapping of A c= downarrow (N . i1) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng the mapping of A or q in downarrow (N . i1) ) assume q in rng the mapping of A ; ::_thesis: q in downarrow (N . i1) then consider x being set such that A11: x in dom the mapping of A and A12: q = the mapping of A . x by FUNCT_1:def_3; reconsider x = x as Element of A by A11; consider y being Element of N such that A13: y = x and A14: t <= y by Def7; A . x = N . y by A13, Th16; hence q in downarrow (N . i1) by A9, A12, A14; ::_thesis: verum end; c is_a_cluster_point_of A proof let O be a_neighborhood of c; :: according to WAYBEL_9:def_9 ::_thesis: A is_often_in O let i be Element of A; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of A st ( i <= b1 & A . b1 in O ) consider i2 being Element of N such that A15: i2 = i and A16: t <= i2 by Def7; N is_often_in O by A4, Def9; then consider j2 being Element of N such that A17: i2 <= j2 and A18: N . j2 in O by WAYBEL_0:def_12; t <= j2 by A16, A17, YELLOW_0:def_2; then reconsider j = j2 as Element of A by Def7; take j ; ::_thesis: ( i <= j & A . j in O ) A is full SubNetStr of N by Th14; hence i <= j by A15, A17, YELLOW_6:12; ::_thesis: A . j in O thus A . j in O by A18, Th16; ::_thesis: verum end; then consider M being subnet of A such that A19: c in Lim M by Th32; reconsider R = rng the mapping of M as Subset of S ; A20: downarrow (N . i1) = { z where z is Element of S : z "\/" (N . i1) = N . i1 } by Lm2; ex f being Function of M,A st ( the mapping of M = the mapping of A * f & ( 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_9; then R c= rng the mapping of A by RELAT_1:26; then R c= downarrow (N . i1) by A10, XBOOLE_1:1; then A21: Cl R c= Cl (downarrow (N . i1)) by PRE_TOPC:19; c in Cl R by A19, Th24; then c in downarrow (N . i1) by A7, A21; then ex z being Element of S st ( c = z & z "\/" (N . i1) = N . i1 ) by A20; hence d <= i by A1, A6, YELLOW_0:24; ::_thesis: verum end; Lm8: for S being Hausdorff compact TopLattice for N being net of S for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds for b being Element of S st rng the mapping of N is_>=_than b holds d >= b proof let S be Hausdorff compact TopLattice; ::_thesis: for N being net of S for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds for b being Element of S st rng the mapping of N is_>=_than b holds d >= b let N be net of S; ::_thesis: for c being Point of S for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds for b being Element of S st rng the mapping of N is_>=_than b holds d >= b let c be Point of S; ::_thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds for b being Element of S st rng the mapping of N is_>=_than b holds d >= b let d be Element of S; ::_thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N implies for b being Element of S st rng the mapping of N is_>=_than b holds d >= b ) assume that A1: c = d and A2: for x being Element of S holds x "/\" is continuous and A3: c is_a_cluster_point_of N ; ::_thesis: for b being Element of S st rng the mapping of N is_>=_than b holds d >= b let b be Element of S; ::_thesis: ( rng the mapping of N is_>=_than b implies d >= b ) assume A4: rng the mapping of N is_>=_than b ; ::_thesis: d >= b A5: now__::_thesis:_for_i_being_Element_of_N_holds_N_._i_in_{b}_"\/"_([#]_S) let i be Element of N; ::_thesis: N . i in {b} "\/" ([#] S) A6: the carrier of N = dom the mapping of N by FUNCT_2:def_1; N . i in rng the mapping of N by A6, FUNCT_1:def_3; then N . i >= b by A4, LATTICE3:def_8; then A7: b "\/" (N . i) = N . i by YELLOW_0:24; b in {b} by TARSKI:def_1; hence N . i in {b} "\/" ([#] S) by A7, YELLOW_4:10; ::_thesis: verum end; A8: rng the mapping of N c= {b} "\/" ([#] S) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng the mapping of N or y in {b} "\/" ([#] S) ) assume y in rng the mapping of N ; ::_thesis: y in {b} "\/" ([#] S) then consider x being set such that A9: x in dom the mapping of N and A10: y = the mapping of N . x by FUNCT_1:def_3; reconsider x = x as Element of N by A9; y = N . x by A10; hence y in {b} "\/" ([#] S) by A5; ::_thesis: verum end; uparrow b is closed by A2, Th27; then {b} "\/" ([#] S) is closed by Th4; then ( {b} "\/" ([#] S) = { (b "\/" y) where y is Element of S : y in [#] S } & c in {b} "\/" ([#] S) ) by A3, A8, Th34, YELLOW_4:15; then ex y being Element of S st ( c = b "\/" y & y in [#] S ) ; hence d >= b by A1, YELLOW_0:22; ::_thesis: verum end; theorem Th36: :: WAYBEL_9:36 for S being Hausdorff compact TopLattice for c being Point of S for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds c = inf N proof let S be Hausdorff compact TopLattice; ::_thesis: for c being Point of S for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds c = inf N let c be Point of S; ::_thesis: for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds c = inf N let N be net of S; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N implies c = inf N ) assume A1: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N ) ; ::_thesis: c = inf N reconsider c9 = c as Element of S ; ( c9 is_<=_than rng the mapping of N & ( for b being Element of S st rng the mapping of N is_>=_than b holds c9 >= b ) ) by A1, Lm7, Lm8; hence c = inf (rng the mapping of N) by YELLOW_0:31 .= inf N by YELLOW_2:def_6 ; ::_thesis: verum end; begin theorem Th37: :: WAYBEL_9:37 for S being Hausdorff TopLattice st ( for N being net of S st N is eventually-directed holds ( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) holds S is meet-continuous proof let S be Hausdorff TopLattice; ::_thesis: ( ( for N being net of S st N is eventually-directed holds ( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) implies S is meet-continuous ) assume that A1: for N being net of S st N is eventually-directed holds ( ex_sup_of N & sup N in Lim N ) and A2: for x being Element of S holds x "/\" is continuous ; ::_thesis: S is meet-continuous for X being non empty directed Subset of S holds ex_sup_of X,S proof let X be non empty directed Subset of S; ::_thesis: ex_sup_of X,S reconsider n = id X as Function of X, the carrier of S by FUNCT_2:7; set N = NetStr(# X,( the InternalRel of S |_2 X),n #); NetStr(# X,( the InternalRel of S |_2 X),n #) is eventually-directed by WAYBEL_2:20; then A3: ex_sup_of NetStr(# X,( the InternalRel of S |_2 X),n #) by A1; rng the mapping of NetStr(# X,( the InternalRel of S |_2 X),n #) = X by RELAT_1:45; hence ex_sup_of X,S by A3, Def3; ::_thesis: verum end; hence S is up-complete by WAYBEL_0:75; :: according to WAYBEL_2:def_7 ::_thesis: S is satisfying_MC for x being Element of S for M being net of S st M is eventually-directed holds x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S)))) proof let x be Element of S; ::_thesis: for M being net of S st M is eventually-directed holds x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S)))) let M be net of S; ::_thesis: ( M is eventually-directed implies x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S)))) ) assume A4: M is eventually-directed ; ::_thesis: x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S)))) A5: sup M in Lim M by A1, A4; then reconsider M1 = M as convergent net of S by YELLOW_6:def_16; set xM = x "/\" M; x "/\" M is eventually-directed by A4, WAYBEL_2:27; then A6: sup (x "/\" M) in Lim (x "/\" M) by A1; x "/\" is continuous by A2; then A7: x "/\" (lim M1) in Lim (x "/\" M1) by Th26; reconsider xM = x "/\" M as convergent net of S by A6, YELLOW_6:def_16; thus x "/\" (sup M) = x "/\" (lim M1) by A5, YELLOW_6:def_17 .= lim xM by A7, YELLOW_6:def_17 .= Sup by A6, YELLOW_6:def_17 .= sup (rng the mapping of xM) by YELLOW_2:def_5 .= sup ({x} "/\" (rng (netmap (M,S)))) by WAYBEL_2:23 ; ::_thesis: verum end; hence S is satisfying_MC by Th9; ::_thesis: verum end; theorem Th38: :: WAYBEL_9:38 for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds for N being net of S st N is eventually-directed holds ( ex_sup_of N & sup N in Lim N ) proof let S be Hausdorff compact TopLattice; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies for N being net of S st N is eventually-directed holds ( ex_sup_of N & sup N in Lim N ) ) assume A1: for x being Element of S holds x "/\" is continuous ; ::_thesis: for N being net of S st N is eventually-directed holds ( ex_sup_of N & sup N in Lim N ) let N be net of S; ::_thesis: ( N is eventually-directed implies ( ex_sup_of N & sup N in Lim N ) ) assume A2: N is eventually-directed ; ::_thesis: ( ex_sup_of N & sup N in Lim N ) A3: for c, d being Point of S st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d proof let c, d be Point of S; ::_thesis: ( c is_a_cluster_point_of N & d is_a_cluster_point_of N implies c = d ) assume that A4: c is_a_cluster_point_of N and A5: d is_a_cluster_point_of N ; ::_thesis: c = d thus c = sup N by A1, A2, A4, Th35 .= d by A1, A2, A5, Th35 ; ::_thesis: verum end; consider c being Point of S such that A6: c is_a_cluster_point_of N by Th30; thus ex_sup_of N ::_thesis: sup N in Lim N proof reconsider d = c as Element of S ; set X = rng the mapping of N; ( rng the mapping of N is_<=_than d & ( for b being Element of S st rng the mapping of N is_<=_than b holds d <= b ) ) by A1, A2, A6, Lm5, Lm6; hence ex_sup_of rng the mapping of N,S by YELLOW_0:15; :: according to WAYBEL_9:def_3 ::_thesis: verum end; c = sup N by A1, A2, A6, Th35; hence sup N in Lim N by A6, A3, Th33; ::_thesis: verum end; theorem Th39: :: WAYBEL_9:39 for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds for N being net of S st N is eventually-filtered holds ( ex_inf_of N & inf N in Lim N ) proof let S be Hausdorff compact TopLattice; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies for N being net of S st N is eventually-filtered holds ( ex_inf_of N & inf N in Lim N ) ) assume A1: for x being Element of S holds x "/\" is continuous ; ::_thesis: for N being net of S st N is eventually-filtered holds ( ex_inf_of N & inf N in Lim N ) let N be net of S; ::_thesis: ( N is eventually-filtered implies ( ex_inf_of N & inf N in Lim N ) ) assume A2: N is eventually-filtered ; ::_thesis: ( ex_inf_of N & inf N in Lim N ) A3: for c, d being Point of S st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d proof let c, d be Point of S; ::_thesis: ( c is_a_cluster_point_of N & d is_a_cluster_point_of N implies c = d ) assume that A4: c is_a_cluster_point_of N and A5: d is_a_cluster_point_of N ; ::_thesis: c = d thus c = inf N by A1, A2, A4, Th36 .= d by A1, A2, A5, Th36 ; ::_thesis: verum end; consider c being Point of S such that A6: c is_a_cluster_point_of N by Th30; thus ex_inf_of N ::_thesis: inf N in Lim N proof reconsider d = c as Element of S ; set X = rng the mapping of N; ( rng the mapping of N is_>=_than d & ( for b being Element of S st rng the mapping of N is_>=_than b holds d >= b ) ) by A1, A2, A6, Lm7, Lm8; hence ex_inf_of rng the mapping of N,S by YELLOW_0:16; :: according to WAYBEL_9:def_4 ::_thesis: verum end; c = inf N by A1, A2, A6, Th36; hence inf N in Lim N by A6, A3, Th33; ::_thesis: verum end; theorem :: WAYBEL_9:40 for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds S is bounded proof let S be Hausdorff compact TopLattice; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies S is bounded ) assume A1: for x being Element of S holds x "/\" is continuous ; ::_thesis: S is bounded thus S is lower-bounded :: according to YELLOW_0:def_6 ::_thesis: S is upper-bounded proof reconsider x = inf (S opp+id) as Element of S ; take x ; :: according to YELLOW_0:def_4 ::_thesis: x is_<=_than the carrier of S A2: rng the mapping of (S opp+id) = rng (id S) by Def6 .= the carrier of S by RELAT_1:45 ; then A3: x = "/\" ( the carrier of S,S) by YELLOW_2:def_6; ex_inf_of S opp+id by A1, Th39; then ex_inf_of the carrier of S,S by A2, Def4; hence x is_<=_than the carrier of S by A3, YELLOW_0:31; ::_thesis: verum end; reconsider x = sup (S +id) as Element of S ; take x ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of S is_<=_than x A4: rng the mapping of (S +id) = rng (id S) by Def5 .= the carrier of S by RELAT_1:45 ; then A5: x = "\/" ( the carrier of S,S) by YELLOW_2:def_5; ex_sup_of S +id by A1, Th38; then ex_sup_of the carrier of S,S by A4, Def3; hence the carrier of S is_<=_than x by A5, YELLOW_0:30; ::_thesis: verum end; theorem :: WAYBEL_9:41 for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds S is meet-continuous proof let S be Hausdorff compact TopLattice; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies S is meet-continuous ) assume A1: for x being Element of S holds x "/\" is continuous ; ::_thesis: S is meet-continuous then for N being net of S st N is eventually-directed holds ( ex_sup_of N & sup N in Lim N ) by Th38; hence S is meet-continuous by A1, Th37; ::_thesis: verum end;