:: YELLOW_6 semantic presentation

begin


definition
let X be set ;
func the_universe_of X ->  set  equals :: YELLOW_6:def 1
 Tarski-Class (the_transitive-closure_of X);
correctness
coherence
Tarski-Class (the_transitive-closure_of X) is set ;
;
end;

:: deftheorem  defines the_universe_of YELLOW_6:def_1_:_
 for X being set holds the_universe_of X = Tarski-Class (the_transitive-closure_of X);

registration
let X be set ;
cluster the_universe_of X ->  epsilon-transitive Tarski ;
coherence
 ( the_universe_of X is epsilon-transitive & the_universe_of X is Tarski ) ;
end;

registration
let X be set ;
cluster the_universe_of X ->  non empty universal ;
coherence
 ( the_universe_of X is universal & not the_universe_of X is empty ) ;
end;

theorem Th1: :: YELLOW_6:1
for T being Universe
for f being Function st dom f in T & rng f c= T holds
product f in T
proof
let T be Universe; ::_thesis: for f being Function st dom f in T & rng f c= T holds
product f in T
let f be Function; ::_thesis: ( dom f in T & rng f c= T implies product f in T )
assume that
A1: dom f in T and
A2: rng f c= T ; ::_thesis: product f in T
 card (dom f) in card T by A1, CLASSES2:1;
then  card (rng f) in card T by CARD_2:61, ORDINAL1:12;
then  rng f in T by A2, CLASSES1:1;
then  union (rng f) in T by CLASSES2:59;
then  Union f in T by CARD_3:def_4;
then  ( product f c= Funcs ((dom f),(Union f)) & Funcs ((dom f),(Union f)) in T ) by A1, CLASSES2:61, FUNCT_6:1;
hence  product f in T by CLASSES1:def_1; ::_thesis: verum
end;

begin

begin

theorem Th2: :: YELLOW_6:2
for Y being non empty set
for J being 1-sorted-yielding ManySortedSet of Y
for i being Element of Y holds (Carrier J) . i = the carrier of (J . i)
proof
let Y be non empty set ; ::_thesis: for J being 1-sorted-yielding ManySortedSet of Y
for i being Element of Y holds (Carrier J) . i = the carrier of (J . i)
let J be 1-sorted-yielding ManySortedSet of Y; ::_thesis: for i being Element of Y holds (Carrier J) . i = the carrier of (J . i)
let i be Element of Y; ::_thesis: (Carrier J) . i = the carrier of (J . i)
 ex R being 1-sorted st
( R = J . i & (Carrier J) . i = the carrier of R ) by PRALG_1:def_13;
hence  (Carrier J) . i = the carrier of (J . i) ; ::_thesis: verum
end;

registration
cluster Relation-like Function-like constant non empty 1-sorted-yielding for set ;
existence
 ex b1 being Function st
( not b1 is empty & b1 is constant & b1 is 1-sorted-yielding )
proof
set S = the 1-sorted ;
take f = {{}} --> the 1-sorted ; ::_thesis: ( not f is empty & f is constant & f is 1-sorted-yielding )
thus  not f is empty ; ::_thesis: ( f is constant & f is 1-sorted-yielding )
thus  f is constant ; ::_thesis: f is 1-sorted-yielding
let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in proj1 f or f . x is 1-sorted )
assume  x in dom f ; ::_thesis: f . x is 1-sorted
hence  f . x is 1-sorted by FUNCOP_1:7; ::_thesis: verum
end;
end;

notation
let J be 1-sorted-yielding Function;
synonym  yielding_non-empty_carriers J for  non-Empty ;
end;

definition
let J be 1-sorted-yielding Function;
redefine attr J is non-Empty  means :Def2: :: YELLOW_6:def 2
 for i being set st i in rng J holds
i is non empty 1-sorted ;
compatibility
 ( J is yielding_non-empty_carriers iff for i being set st i in rng J holds
i is non empty 1-sorted )
proof
hereby  ::_thesis: ( ( for i being set st i in rng J holds
i is non empty 1-sorted ) implies J is yielding_non-empty_carriers )
assume A1: J is non-Empty ; ::_thesis: for i being set st i in rng J holds
i is non empty 1-sorted
let i be set ; ::_thesis: ( i in rng J implies i is non empty 1-sorted )
assume A2: i in rng J ; ::_thesis: i is non empty 1-sorted
then  ex x being set st
( x in dom J & i = J . x ) by FUNCT_1:def_3;
hence  i is non empty 1-sorted by A1, A2, PRALG_1:def_11, WAYBEL_3:def_7; ::_thesis: verum
end;
assume A3: for i being set st i in rng J holds
i is non empty 1-sorted ; ::_thesis: J is yielding_non-empty_carriers
let S be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not S in proj2 J or not S is empty )
thus  ( not S in proj2 J or not S is empty ) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines yielding_non-empty_carriers YELLOW_6:def_2_:_
 for J being 1-sorted-yielding Function holds
( J is yielding_non-empty_carriers iff for i being set st i in rng J holds
i is non empty 1-sorted );

registration
let X be set ;
let L be 1-sorted ;
clusterX --> L ->  1-sorted-yielding ;
coherence
 X --> L is 1-sorted-yielding
proof
let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in proj1 (X --> L) or (X --> L) . x is 1-sorted )
set IT = X --> L;
assume  x in dom (X --> L) ; ::_thesis: (X --> L) . x is 1-sorted
then  (X --> L) . x in rng (X --> L) by FUNCT_1:def_3;
hence  (X --> L) . x is 1-sorted by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) 1-sorted-yielding yielding_non-empty_carriers for set ;
existence
 ex b1 being 1-sorted-yielding ManySortedSet of I st b1 is yielding_non-empty_carriers
proof
set R = the non empty 1-sorted ;
take  I --> the non empty 1-sorted ; ::_thesis: I --> the non empty 1-sorted is yielding_non-empty_carriers
let i be set ; :: according to YELLOW_6:def_2 ::_thesis: ( i in rng (I --> the non empty 1-sorted ) implies i is non empty 1-sorted )
assume  i in rng (I --> the non empty 1-sorted ) ; ::_thesis: i is non empty 1-sorted
hence  i is non empty 1-sorted by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let J be RelStr-yielding ManySortedSet of I;
cluster the carrier of (product J) ->  functional ;
coherence
 the carrier of (product J) is functional
proof
 product (Carrier J) is functional ;
hence  the carrier of (product J) is functional by YELLOW_1:def_4; ::_thesis: verum
end;
end;

registration
let I be set ;
let J be 1-sorted-yielding yielding_non-empty_carriers ManySortedSet of I;
cluster Carrier J -> V2() ;
coherence
 Carrier J is non-empty
proof
assume  {} in rng (Carrier J) ; :: according to RELAT_1:def_9 ::_thesis: contradiction
then consider i being set  such that
A1: i in dom (Carrier J) and
A2: (Carrier J) . i = {} by FUNCT_1:def_3;
A3: i in I by A1;
then consider R being 1-sorted  such that
A4: R = J . i and
A5: (Carrier J) . i = the carrier of R by PRALG_1:def_13;
A6: R is empty by A2, A5;
 i in dom J by A3, PARTFUN1:def_2;
then  R in rng J by A4, FUNCT_1:def_3;
hence  contradiction by A6, Def2; ::_thesis: verum
end;
end;

begin

registration
let T be non empty RelStr ;
let A be lower Subset of T;
clusterA `  ->  upper ;
coherence
 A ` is upper
proof
let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A ` or not x <= y or y in A ` )
assume that
A1: x in A ` and
A2: x <= y ; ::_thesis: y in A `
 not x in A by A1, XBOOLE_0:def_5;
then  not y in A by A2, WAYBEL_0:def_19;
hence  y in A ` by XBOOLE_0:def_5; ::_thesis: verum
end;
end;

registration
let T be non empty RelStr ;
let A be upper Subset of T;
clusterA `  ->  lower ;
coherence
 A ` is lower
proof
let x, y be Element of T; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in A ` or not y <= x or y in A ` )
assume that
A1: x in A ` and
A2: y <= x ; ::_thesis: y in A `
 not x in A by A1, XBOOLE_0:def_5;
then  not y in A by A2, WAYBEL_0:def_20;
hence  y in A ` by XBOOLE_0:def_5; ::_thesis: verum
end;
end;

definition
let N be non empty RelStr ;
redefine attr N is directed  means :Def3: :: YELLOW_6:def 3
 for x, y being Element of N ex z being Element of N st
( x <= z & y <= z );
compatibility
 ( N is directed iff for x, y being Element of N ex z being Element of N st
( x <= z & y <= z ) )
proof
hereby  ::_thesis: ( ( for x, y being Element of N ex z being Element of N st
( x <= z & y <= z ) ) implies N is directed )
assume A1: N is directed ; ::_thesis: for x, y being Element of N ex z being Element of N st
( x <= z & y <= z )
let x, y be Element of N; ::_thesis: ex z being Element of N st
( x <= z & y <= z )
 [#] N is directed by A1, WAYBEL_0:def_6;
then  ex z being Element of N st
( z in [#] N & x <= z & y <= z ) by WAYBEL_0:def_1;
hence  ex z being Element of N st
( x <= z & y <= z ) ; ::_thesis: verum
end;
assume A2: for x, y being Element of N ex z being Element of N st
( x <= z & y <= z ) ; ::_thesis: N is directed
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 )
consider z being Element of N such that
A3: ( x <= z & y <= z ) by A2;
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 A3; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines directed YELLOW_6:def_3_:_
 for N being non empty RelStr holds
( N is directed iff for x, y being Element of N ex z being Element of N st
( x <= z & y <= z ) );

registration
let X be set ;
cluster BoolePoset X ->  directed ;
coherence
 BoolePoset X is directed
proof
let x, y be Element of (BoolePoset X); :: according to YELLOW_6:def_3 ::_thesis: ex z being Element of (BoolePoset X) st
( x <= z & y <= z )
take  x "\/" y ; ::_thesis: ( x <= x "\/" y & y <= x "\/" y )
A1: y c= x \/ y by XBOOLE_1:7;
 ( x "\/" y = x \/ y & x c= x \/ y ) by XBOOLE_1:7, YELLOW_1:17;
hence  ( x <= x "\/" y & y <= x "\/" y ) by A1, YELLOW_1:2; ::_thesis: verum
end;
end;

registration
cluster non empty strict transitive directed for RelStr ;
existence
 ex b1 being RelStr st
( not b1 is empty & b1 is directed & b1 is transitive & b1 is strict )
proof
take  BoolePoset {} ; ::_thesis: ( not BoolePoset {} is empty & BoolePoset {} is directed & BoolePoset {} is transitive & BoolePoset {} is strict )
thus  ( not BoolePoset {} is empty & BoolePoset {} is directed & BoolePoset {} is transitive & BoolePoset {} is strict ) ; ::_thesis: verum
end;
end;

Lm1:  for N being non empty RelStr holds
( N is directed iff RelStr(# the carrier of N, the InternalRel of N #) is directed )
proof
let N be non empty RelStr ; ::_thesis: ( N is directed iff RelStr(# the carrier of N, the InternalRel of N #) is directed )
thus  ( N is directed implies RelStr(# the carrier of N, the InternalRel of N #) is directed ) ::_thesis: ( RelStr(# the carrier of N, the InternalRel of N #) is directed implies N is directed )
proof
assume A1: N is directed ; ::_thesis: RelStr(# the carrier of N, the InternalRel of N #) is directed
let x, y be Element of RelStr(# the carrier of N, the InternalRel of N #); :: according to YELLOW_6:def_3 ::_thesis: ex z being Element of RelStr(# the carrier of N, the InternalRel of N #) st
( x <= z & y <= z )
reconsider x9 = x, y9 = y as Element of N ;
consider z9 being Element of N such that
A2: ( x9 <= z9 & y9 <= z9 ) by A1, Def3;
reconsider z = z9 as Element of RelStr(# the carrier of N, the InternalRel of N #) ;
take  z ; ::_thesis: ( x <= z & y <= z )
 ( [x,z] in the InternalRel of N & [y,z] in the InternalRel of N ) by A2, ORDERS_2:def_5;
hence  ( x <= z & y <= z ) by ORDERS_2:def_5; ::_thesis: verum
end;
assume A3: RelStr(# the carrier of N, the InternalRel of N #) is directed ; ::_thesis: N is directed
let x, y be Element of N; :: according to YELLOW_6:def_3 ::_thesis: ex z being Element of N st
( x <= z & y <= z )
reconsider x9 = x, y9 = y as Element of RelStr(# the carrier of N, the InternalRel of N #) ;
consider z9 being Element of RelStr(# the carrier of N, the InternalRel of N #) such that
A4: ( x9 <= z9 & y9 <= z9 ) by A3, Def3;
reconsider z = z9 as Element of N ;
take  z ; ::_thesis: ( x <= z & y <= z )
 ( [x9,z9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) & [y9,z9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) ) by A4, ORDERS_2:def_5;
hence  ( x <= z & y <= z ) by ORDERS_2:def_5; ::_thesis: verum
end;

Lm2:  for N being non empty RelStr holds
( N is transitive iff RelStr(# the carrier of N, the InternalRel of N #) is transitive )
proof
let N be non empty RelStr ; ::_thesis: ( N is transitive iff RelStr(# the carrier of N, the InternalRel of N #) is transitive )
thus  ( N is transitive implies RelStr(# the carrier of N, the InternalRel of N #) is transitive ) ::_thesis: ( RelStr(# the carrier of N, the InternalRel of N #) is transitive implies N is transitive )
proof
assume A1: N is transitive ; ::_thesis: RelStr(# the carrier of N, the InternalRel of N #) is transitive
let x, y, z be Element of RelStr(# the carrier of N, the InternalRel of N #); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A2: x <= y and
A3: y <= z ; ::_thesis: x <= z
reconsider x9 = x, y9 = y, z9 = z as Element of N ;
 [y,z] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) by A3, ORDERS_2:def_5;
then A4: y9 <= z9 by ORDERS_2:def_5;
 [x,y] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) by A2, ORDERS_2:def_5;
then  x9 <= y9 by ORDERS_2:def_5;
then  x9 <= z9 by A1, A4, YELLOW_0:def_2;
then  [x9,z9] in the InternalRel of N by ORDERS_2:def_5;
hence  x <= z by ORDERS_2:def_5; ::_thesis: verum
end;
assume A5: RelStr(# the carrier of N, the InternalRel of N #) is transitive ; ::_thesis: N is transitive
let x, y, z be Element of N; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A6: x <= y and
A7: y <= z ; ::_thesis: x <= z
reconsider x9 = x, y9 = y, z9 = z as Element of RelStr(# the carrier of N, the InternalRel of N #) ;
 [y9,z9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) by A7, ORDERS_2:def_5;
then A8: y9 <= z9 by ORDERS_2:def_5;
 [x9,y9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #) by A6, ORDERS_2:def_5;
then  x9 <= y9 by ORDERS_2:def_5;
then  x9 <= z9 by A5, A8, YELLOW_0:def_2;
then  [x,z] in the InternalRel of N by ORDERS_2:def_5;
hence  x <= z by ORDERS_2:def_5; ::_thesis: verum
end;

definition
let M be non empty set ;
let N be non empty RelStr ;
let f be Function of M, the carrier of N;
let m be Element of M;
:: original: .
redefine funcf . m ->  Element of N;
coherence
 f . m is Element of N
proof
 f . m is Element of N ;
hence  f . m is Element of N ; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) 1-sorted-yielding RelStr-yielding yielding_non-empty_carriers for set ;
existence
 ex b1 being RelStr-yielding ManySortedSet of I st b1 is yielding_non-empty_carriers
proof
set R = the non empty RelStr ;
take  I --> the non empty RelStr ; ::_thesis: I --> the non empty RelStr is yielding_non-empty_carriers
let i be set ; :: according to YELLOW_6:def_2 ::_thesis: ( i in rng (I --> the non empty RelStr ) implies i is non empty 1-sorted )
assume  i in rng (I --> the non empty RelStr ) ; ::_thesis: i is non empty 1-sorted
hence  i is non empty 1-sorted by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let J be RelStr-yielding yielding_non-empty_carriers ManySortedSet of I;
cluster product J ->  non empty ;
coherence
 not product J is empty ;
end;

registration
let Y1, Y2 be directed RelStr ;
cluster[:Y1,Y2:] ->  directed ;
coherence
 [:Y1,Y2:] is directed
proof
reconsider S2 = [#] Y2 as directed Subset of Y2 by WAYBEL_0:def_6;
reconsider S1 = [#] Y1 as directed Subset of Y1 by WAYBEL_0:def_6;
 [:S1,S2:] is directed ;
then  [#] [:Y1,Y2:] is directed by YELLOW_3:def_2;
hence  [:Y1,Y2:] is directed by WAYBEL_0:def_6; ::_thesis: verum
end;
end;

theorem Th3: :: YELLOW_6:3
for R being RelStr holds the carrier of R = the carrier of (R ~)
proof
let R be RelStr ; ::_thesis: the carrier of R = the carrier of (R ~)
 R ~ = RelStr(# the carrier of R,( the InternalRel of R ~) #) by LATTICE3:def_5;
hence  the carrier of R = the carrier of (R ~) ; ::_thesis: verum
end;

Lm3:  for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
proof
let R, S be RelStr ; ::_thesis: for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
let p, q be Element of R; ::_thesis: for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
let p9, q9 be Element of S; ::_thesis: ( p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q implies p9 <= q9 )
assume A1: ( p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) ) ; ::_thesis: ( not p <= q or p9 <= q9 )
assume  p <= q ; ::_thesis: p9 <= q9
then  [p9,q9] in the InternalRel of S by A1, ORDERS_2:def_5;
hence  p9 <= q9 by ORDERS_2:def_5; ::_thesis: verum
end;

definition
let S be 1-sorted ;
let N be NetStr over S;
attrN is constant  means :Def4: :: YELLOW_6:def 4
 the mapping of N is constant ;
end;

:: deftheorem Def4 defines constant YELLOW_6:def_4_:_
 for S being 1-sorted
for N being NetStr over S holds
( N is constant iff the mapping of N is constant );

definition
let R be RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
func ConstantNet (R,p) ->  strict NetStr over T means :Def5: :: YELLOW_6:def 5
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of it = the carrier of it --> p );
existence
 ex b1 being strict NetStr over T st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = the carrier of b1 --> p )
proof
reconsider f = the carrier of R --> p as Function of the carrier of R, the carrier of T ;
take  NetStr(# the carrier of R, the InternalRel of R,f #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of R, the InternalRel of R,f #), the InternalRel of NetStr(# the carrier of R, the InternalRel of R,f #) #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of NetStr(# the carrier of R, the InternalRel of R,f #) = the carrier of NetStr(# the carrier of R, the InternalRel of R,f #) --> p )
thus  ( RelStr(# the carrier of NetStr(# the carrier of R, the InternalRel of R,f #), the InternalRel of NetStr(# the carrier of R, the InternalRel of R,f #) #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of NetStr(# the carrier of R, the InternalRel of R,f #) = the carrier of NetStr(# the carrier of R, the InternalRel of R,f #) --> p ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict NetStr over T st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = the carrier of b1 --> p & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b2 = the carrier of b2 --> p holds
b1 = b2;
;
end;

:: deftheorem Def5 defines ConstantNet YELLOW_6:def_5_:_
 for R being RelStr
for T being non empty 1-sorted
for p being Element of T
for b4 being strict NetStr over T holds
( b4 = ConstantNet (R,p) iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b4 = the carrier of b4 --> p ) );

registration
let R be RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
cluster ConstantNet (R,p) ->  strict constant ;
coherence
 ConstantNet (R,p) is constant
proof
 the carrier of (ConstantNet (R,p)) --> p is constant ;
hence  the mapping of (ConstantNet (R,p)) is constant by Def5; :: according to YELLOW_6:def_4 ::_thesis: verum
end;
end;

registration
let R be non empty RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
cluster ConstantNet (R,p) ->  non empty strict ;
coherence
 not ConstantNet (R,p) is empty
proof
 RelStr(# the carrier of (ConstantNet (R,p)), the InternalRel of (ConstantNet (R,p)) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def5;
hence  not the carrier of (ConstantNet (R,p)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
let R be non empty directed RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
cluster ConstantNet (R,p) ->  strict directed ;
coherence
 ConstantNet (R,p) is directed
proof
 ( RelStr(# the carrier of (ConstantNet (R,p)), the InternalRel of (ConstantNet (R,p)) #) = RelStr(# the carrier of R, the InternalRel of R #) & RelStr(# the carrier of R, the InternalRel of R #) is directed ) by Def5, Lm1;
hence  ConstantNet (R,p) is directed by Lm1; ::_thesis: verum
end;
end;

registration
let R be non empty transitive RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
cluster ConstantNet (R,p) ->  transitive strict ;
coherence
 ConstantNet (R,p) is transitive
proof
 ( RelStr(# the carrier of (ConstantNet (R,p)), the InternalRel of (ConstantNet (R,p)) #) = RelStr(# the carrier of R, the InternalRel of R #) & RelStr(# the carrier of R, the InternalRel of R #) is transitive ) by Def5, Lm2;
hence  ConstantNet (R,p) is transitive by Lm2; ::_thesis: verum
end;
end;

theorem Th4: :: YELLOW_6:4
for R being RelStr
for T being non empty 1-sorted
for p being Element of T holds the carrier of (ConstantNet (R,p)) = the carrier of R
proof
let R be RelStr ; ::_thesis: for T being non empty 1-sorted
for p being Element of T holds the carrier of (ConstantNet (R,p)) = the carrier of R
let T be non empty 1-sorted ; ::_thesis: for p being Element of T holds the carrier of (ConstantNet (R,p)) = the carrier of R
let p be Element of T; ::_thesis: the carrier of (ConstantNet (R,p)) = the carrier of R
 RelStr(# the carrier of (ConstantNet (R,p)), the InternalRel of (ConstantNet (R,p)) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def5;
hence  the carrier of (ConstantNet (R,p)) = the carrier of R ; ::_thesis: verum
end;

theorem Th5: :: YELLOW_6:5
for R being non empty RelStr
for T being non empty 1-sorted
for p being Element of T
for q being Element of (ConstantNet (R,p)) holds (ConstantNet (R,p)) . q = p
proof
let R be non empty RelStr ; ::_thesis: for T being non empty 1-sorted
for p being Element of T
for q being Element of (ConstantNet (R,p)) holds (ConstantNet (R,p)) . q = p
let T be non empty 1-sorted ; ::_thesis: for p being Element of T
for q being Element of (ConstantNet (R,p)) holds (ConstantNet (R,p)) . q = p
let p be Element of T; ::_thesis: for q being Element of (ConstantNet (R,p)) holds (ConstantNet (R,p)) . q = p
let q be Element of (ConstantNet (R,p)); ::_thesis: (ConstantNet (R,p)) . q = p
thus (ConstantNet (R,p)) . q = ( the carrier of (ConstantNet (R,p)) --> p) . q by Def5
.= p by FUNCOP_1:7 ; ::_thesis: verum
end;

registration
let T be non empty 1-sorted ;
let N be non empty NetStr over T;
cluster the mapping of N ->  non empty ;
coherence
 not the mapping of N is empty ;
end;

begin

theorem Th6: :: YELLOW_6:6
for R being RelStr holds R is full SubRelStr of R
proof
let R be RelStr ; ::_thesis: R is full SubRelStr of R
 the InternalRel of R c= the InternalRel of R ;
then reconsider R9 = R as SubRelStr of R by YELLOW_0:def_13;
 the InternalRel of R9 = the InternalRel of R |_2 the carrier of R9 by XBOOLE_1:28;
hence  R is full SubRelStr of R by YELLOW_0:def_14; ::_thesis: verum
end;

theorem Th7: :: YELLOW_6:7
for R being RelStr
for S being SubRelStr of R
for T being SubRelStr of S holds T is SubRelStr of R
proof
let R be RelStr ; ::_thesis: for S being SubRelStr of R
for T being SubRelStr of S holds T is SubRelStr of R
let S be SubRelStr of R; ::_thesis: for T being SubRelStr of S holds T is SubRelStr of R
let T be SubRelStr of S; ::_thesis: T is SubRelStr of R
 ( the InternalRel of S c= the InternalRel of R & the InternalRel of T c= the InternalRel of S ) by YELLOW_0:def_13;
then A1: the InternalRel of T c= the InternalRel of R by XBOOLE_1:1;
 ( the carrier of S c= the carrier of R & the carrier of T c= the carrier of S ) by YELLOW_0:def_13;
then  the carrier of T c= the carrier of R by XBOOLE_1:1;
hence  T is SubRelStr of R by A1, YELLOW_0:def_13; ::_thesis: verum
end;

definition
let S be 1-sorted ;
let N be NetStr over S;
mode SubNetStr of N ->  NetStr over S means :Def6: :: YELLOW_6:def 6
( it is SubRelStr of N & the mapping of it = the mapping of N | the carrier of it );
existence
 ex b1 being NetStr over S st
( b1 is SubRelStr of N & the mapping of b1 = the mapping of N | the carrier of b1 )
proof
take  N ; ::_thesis: ( N is SubRelStr of N & the mapping of N = the mapping of N | the carrier of N )
thus  N is SubRelStr of N by Th6; ::_thesis: the mapping of N = the mapping of N | the carrier of N
thus  the mapping of N = the mapping of N | the carrier of N ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines SubNetStr YELLOW_6:def_6_:_
 for S being 1-sorted
for N, b3 being NetStr over S holds
( b3 is SubNetStr of N iff ( b3 is SubRelStr of N & the mapping of b3 = the mapping of N | the carrier of b3 ) );

theorem :: YELLOW_6:8
for S being 1-sorted
for N being NetStr over S holds N is SubNetStr of N
proof
let S be 1-sorted ; ::_thesis: for N being NetStr over S holds N is SubNetStr of N
let N be NetStr over S; ::_thesis: N is SubNetStr of N
 ( N is SubRelStr of N & the mapping of N = the mapping of N | the carrier of N ) by Th6;
hence  N is SubNetStr of N by Def6; ::_thesis: verum
end;

theorem :: YELLOW_6:9
for Q being 1-sorted
for R being NetStr over Q
for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R
proof
let Q be 1-sorted ; ::_thesis: for R being NetStr over Q
for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R
let R be NetStr over Q; ::_thesis: for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R
let S be SubNetStr of R; ::_thesis: for T being SubNetStr of S holds T is SubNetStr of R
let T be SubNetStr of S; ::_thesis: T is SubNetStr of R
A1: T is SubRelStr of S by Def6;
then A2: the carrier of T c= the carrier of S by YELLOW_0:def_13;
A3: the mapping of T = the mapping of S | the carrier of T by Def6
.= ( the mapping of R | the carrier of S) | the carrier of T by Def6
.= the mapping of R | ( the carrier of S /\ the carrier of T) by RELAT_1:71
.= the mapping of R | the carrier of T by A2, XBOOLE_1:28 ;
 S is SubRelStr of R by Def6;
then  T is SubRelStr of R by A1, Th7;
hence  T is SubNetStr of R by A3, Def6; ::_thesis: verum
end;

Lm4:  for S being 1-sorted
for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is SubNetStr of R
proof
let S be 1-sorted ; ::_thesis: for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is SubNetStr of R
let N be NetStr over S; ::_thesis: NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is SubNetStr of N
 ( NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is SubRelStr of N & the mapping of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = the mapping of N | the carrier of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) ) by RELSET_1:19, YELLOW_0:def_13;
hence  NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is SubNetStr of N by Def6; ::_thesis: verum
end;

definition
let S be 1-sorted ;
let N be NetStr over S;
let M be SubNetStr of N;
attrM is full  means :Def7: :: YELLOW_6:def 7
M is full SubRelStr of N;
end;

:: deftheorem Def7 defines full YELLOW_6:def_7_:_
 for S being 1-sorted
for N being NetStr over S
for M being SubNetStr of N holds
( M is full iff M is full SubRelStr of N );

Lm5:  for S being 1-sorted
for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
proof
let S be 1-sorted ; ::_thesis: for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
let R be NetStr over S; ::_thesis: NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
reconsider R9 = NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) as SubRelStr of R by YELLOW_0:def_13;
 the InternalRel of R9 = the InternalRel of R |_2 the carrier of R9 by XBOOLE_1:28;
hence  NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R by YELLOW_0:def_14; ::_thesis: verum
end;

registration
let S be 1-sorted ;
let N be NetStr over S;
cluster strict full for SubNetStr of N;
existence
 ex b1 being SubNetStr of N st
( b1 is full & b1 is strict )
proof
reconsider M = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) as SubNetStr of N by Lm4;
take  M ; ::_thesis: ( M is full & M is strict )
thus  M is full SubRelStr of N by Lm5; :: according to YELLOW_6:def_7 ::_thesis: M is strict
thus  M is strict ; ::_thesis: verum
end;
end;

registration
let S be 1-sorted ;
let N be non empty NetStr over S;
cluster non empty strict full for SubNetStr of N;
existence
 ex b1 being SubNetStr of N st
( b1 is full & not b1 is empty & b1 is strict )
proof
reconsider M = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) as SubNetStr of N by Lm4;
take  M ; ::_thesis: ( M is full & not M is empty & M is strict )
thus  M is full SubRelStr of N by Lm5; :: according to YELLOW_6:def_7 ::_thesis: ( not M is empty & M is strict )
thus  ( not M is empty & M is strict ) ; ::_thesis: verum
end;
end;

theorem Th10: :: YELLOW_6:10
for S being 1-sorted
for N being NetStr over S
for M being SubNetStr of N holds the carrier of M c= the carrier of N
proof
let S be 1-sorted ; ::_thesis: for N being NetStr over S
for M being SubNetStr of N holds the carrier of M c= the carrier of N
let N be NetStr over S; ::_thesis: for M being SubNetStr of N holds the carrier of M c= the carrier of N
let M be SubNetStr of N; ::_thesis: the carrier of M c= the carrier of N
 M is SubRelStr of N by Def6;
hence  the carrier of M c= the carrier of N by YELLOW_0:def_13; ::_thesis: verum
end;

theorem Th11: :: YELLOW_6:11
for S being 1-sorted
for N being NetStr over S
for M being SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
proof
let S be 1-sorted ; ::_thesis: for N being NetStr over S
for M being SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
let N be NetStr over S; ::_thesis: for M being SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
let M be SubNetStr of N; ::_thesis: for x, y being Element of N
for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
let x, y be Element of N; ::_thesis: for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
let i, j be Element of M; ::_thesis: ( x = i & y = j & i <= j implies x <= y )
assume that
A1: ( x = i & y = j ) and
A2: i <= j ; ::_thesis: x <= y
reconsider M = M as SubRelStr of N by Def6;
reconsider i9 = i, j9 = j as Element of M ;
 i9 <= j9 by A2;
hence  x <= y by A1, YELLOW_0:59; ::_thesis: verum
end;

theorem Th12: :: YELLOW_6:12
for S being 1-sorted
for N being non empty NetStr over S
for M being non empty full SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
proof
let S be 1-sorted ; ::_thesis: for N being non empty NetStr over S
for M being non empty full SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let N be non empty NetStr over S; ::_thesis: for M being non empty full SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let M be non empty full SubNetStr of N; ::_thesis: for x, y being Element of N
for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let x, y be Element of N; ::_thesis: for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let i, j be Element of M; ::_thesis: ( x = i & y = j & x <= y implies i <= j )
assume A1: ( x = i & y = j & x <= y ) ; ::_thesis: i <= j
reconsider M = M as non empty full SubRelStr of N by Def7;
reconsider i9 = i, j9 = j as Element of M ;
 i9 <= j9 by A1, YELLOW_0:60;
hence  i <= j ; ::_thesis: verum
end;

begin

registration
let T be non empty 1-sorted ;
cluster non empty transitive strict directed constant for NetStr over T;
existence
 ex b1 being net of T st
( b1 is constant & b1 is strict )
proof
set R = the non empty transitive directed RelStr ;
set p = the Element of T;
take  ConstantNet ( the non empty transitive directed RelStr , the Element of T) ; ::_thesis: ( ConstantNet ( the non empty transitive directed RelStr , the Element of T) is constant & ConstantNet ( the non empty transitive directed RelStr , the Element of T) is strict )
thus  ( ConstantNet ( the non empty transitive directed RelStr , the Element of T) is constant & ConstantNet ( the non empty transitive directed RelStr , the Element of T) is strict ) ; ::_thesis: verum
end;
end;

registration
let T be non empty 1-sorted ;
let N be constant NetStr over T;
cluster the mapping of N ->  constant ;
coherence
 the mapping of N is constant by Def4;
end;

definition
let T be non empty 1-sorted ;
let N be NetStr over T;
assume A1: ( N is constant & not N is empty ) ;
func the_value_of N ->  Element of T equals :Def8: :: YELLOW_6:def 8
 the_value_of the mapping of N;
coherence
 the_value_of the mapping of N is Element of T
proof
reconsider M = N as non empty constant NetStr over T by A1;
set f = the mapping of M;
 ex x being set st
( x in dom the mapping of M & the_value_of the mapping of M = the mapping of M . x ) by FUNCT_1:def_12;
then  the_value_of the mapping of M in rng the mapping of M by FUNCT_1:def_3;
hence  the_value_of the mapping of N is Element of T ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines the_value_of YELLOW_6:def_8_:_
 for T being non empty 1-sorted
for N being NetStr over T st N is constant & not N is empty holds
the_value_of N = the_value_of the mapping of N;

theorem Th13: :: YELLOW_6:13
for R being non empty RelStr
for T being non empty 1-sorted
for p being Element of T holds the_value_of (ConstantNet (R,p)) = p
proof
let R be non empty RelStr ; ::_thesis: for T being non empty 1-sorted
for p being Element of T holds the_value_of (ConstantNet (R,p)) = p
let T be non empty 1-sorted ; ::_thesis: for p being Element of T holds the_value_of (ConstantNet (R,p)) = p
let p be Element of T; ::_thesis: the_value_of (ConstantNet (R,p)) = p
thus  the_value_of (ConstantNet (R,p)) = the_value_of the mapping of (ConstantNet (R,p)) by Def8
.= the_value_of ( the carrier of (ConstantNet (R,p)) --> p) by Def5
.= p by FUNCOP_1:79 ; ::_thesis: verum
end;

definition
let T be non empty 1-sorted ;
let N be net of T;
mode subnet of N ->  net of T means :Def9: :: YELLOW_6:def 9
 ex f being Function of it,N st
( the mapping of it = the mapping of N * f & ( for m being Element of N ex n being Element of it st
for p being Element of it st n <= p holds
m <= f . p ) );
existence
 ex b1 being net of T ex f being Function of b1,N st
( the mapping of b1 = the mapping of N * f & ( for m being Element of N ex n being Element of b1 st
for p being Element of b1 st n <= p holds
m <= f . p ) )
proof
take  N ; ::_thesis: ex f being Function of N,N st
( the mapping of N = the mapping of N * f & ( for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= f . p ) )
take  id N ; ::_thesis: ( the mapping of N = the mapping of N * (id N) & ( for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p ) )
thus  the mapping of N = the mapping of N * (id N) by FUNCT_2:17; ::_thesis: for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p
let m be Element of N; ::_thesis: ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p
take n = m; ::_thesis: for p being Element of N st n <= p holds
m <= (id N) . p
let p be Element of N; ::_thesis: ( n <= p implies m <= (id N) . p )
assume  n <= p ; ::_thesis: m <= (id N) . p
hence  m <= (id N) . p by FUNCT_1:18; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines subnet YELLOW_6:def_9_:_
 for T being non empty 1-sorted
for N, b3 being net of T holds
( b3 is subnet of N iff ex f being Function of b3,N st
( the mapping of b3 = the mapping of N * f & ( for m being Element of N ex n being Element of b3 st
for p being Element of b3 st n <= p holds
m <= f . p ) ) );

theorem :: YELLOW_6:14
for T being non empty 1-sorted
for N being net of T holds N is subnet of N
proof
let T be non empty 1-sorted ; ::_thesis: for N being net of T holds N is subnet of N
let N be net of T; ::_thesis: N is subnet of N
take  id N ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of N = the mapping of N * (id N) & ( for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p ) )
thus  the mapping of N = the mapping of N * (id N) by FUNCT_2:17; ::_thesis: for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p
let m be Element of N; ::_thesis: ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p
take n = m; ::_thesis: for p being Element of N st n <= p holds
m <= (id N) . p
let p be Element of N; ::_thesis: ( n <= p implies m <= (id N) . p )
assume  n <= p ; ::_thesis: m <= (id N) . p
hence  m <= (id N) . p by FUNCT_1:18; ::_thesis: verum
end;

theorem :: YELLOW_6:15
for T being non empty 1-sorted
for N1, N2, N3 being net of T st N1 is subnet of N2 & N2 is subnet of N3 holds
N1 is subnet of N3
proof
let T be non empty 1-sorted ; ::_thesis: for N1, N2, N3 being net of T st N1 is subnet of N2 & N2 is subnet of N3 holds
N1 is subnet of N3
let N1, N2, N3 be net of T; ::_thesis: ( N1 is subnet of N2 & N2 is subnet of N3 implies N1 is subnet of N3 )
given f being Function of N1,N2 such that A1: the mapping of N1 = the mapping of N2 * f and
A2: for m being Element of N2 ex n being Element of N1 st
for p being Element of N1 st n <= p holds
m <= f . p ; :: according to YELLOW_6:def_9 ::_thesis: ( not N2 is subnet of N3 or N1 is subnet of N3 )
given g being Function of N2,N3 such that A3: the mapping of N2 = the mapping of N3 * g and
A4: for m being Element of N3 ex n being Element of N2 st
for p being Element of N2 st n <= p holds
m <= g . p ; :: according to YELLOW_6:def_9 ::_thesis: N1 is subnet of N3
take  g * f ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of N1 = the mapping of N3 * (g * f) & ( for m being Element of N3 ex n being Element of N1 st
for p being Element of N1 st n <= p holds
m <= (g * f) . p ) )
thus  the mapping of N1 = the mapping of N3 * (g * f) by A1, A3, RELAT_1:36; ::_thesis: for m being Element of N3 ex n being Element of N1 st
for p being Element of N1 st n <= p holds
m <= (g * f) . p
let m be Element of N3; ::_thesis: ex n being Element of N1 st
for p being Element of N1 st n <= p holds
m <= (g * f) . p
consider m1 being Element of N2 such that
A5: for p being Element of N2 st m1 <= p holds
m <= g . p by A4;
consider n being Element of N1 such that
A6: for p being Element of N1 st n <= p holds
m1 <= f . p by A2;
take  n ; ::_thesis: for p being Element of N1 st n <= p holds
m <= (g * f) . p
let p be Element of N1; ::_thesis: ( n <= p implies m <= (g * f) . p )
assume  n <= p ; ::_thesis: m <= (g * f) . p
then  m <= g . (f . p) by A5, A6;
hence  m <= (g * f) . p by FUNCT_2:15; ::_thesis: verum
end;

theorem Th16: :: YELLOW_6:16
for T being non empty 1-sorted
for N being constant net of T
for i being Element of N holds N . i = the_value_of N
proof
let T be non empty 1-sorted ; ::_thesis: for N being constant net of T
for i being Element of N holds N . i = the_value_of N
let N be constant net of T; ::_thesis: for i being Element of N holds N . i = the_value_of N
let i be Element of N; ::_thesis: N . i = the_value_of N
 dom the mapping of N = the carrier of N by FUNCT_2:def_1;
hence N . i = the_value_of the mapping of N by FUNCT_1:def_12
.= the_value_of N by Def8 ;
::_thesis: verum
end;

theorem Th17: :: YELLOW_6:17
for L being non empty 1-sorted
for N being net of L
for X, Y being set st N is_eventually_in X & N is_eventually_in Y holds
X meets Y
proof
let L be non empty 1-sorted ; ::_thesis: for N being net of L
for X, Y being set st N is_eventually_in X & N is_eventually_in Y holds
X meets Y
let N be net of L; ::_thesis: for X, Y being set st N is_eventually_in X & N is_eventually_in Y holds
X meets Y
let X, Y be set ; ::_thesis: ( N is_eventually_in X & N is_eventually_in Y implies X meets Y )
assume  N is_eventually_in X ; ::_thesis: ( not N is_eventually_in Y or X meets Y )
then consider i1 being Element of N such that
A1: for j being Element of N st i1 <= j holds
N . j in X by WAYBEL_0:def_11;
assume  N is_eventually_in Y ; ::_thesis: X meets Y
then consider i2 being Element of N such that
A2: for j being Element of N st i2 <= j holds
N . j in Y by WAYBEL_0:def_11;
consider i being Element of N such that
A3: i1 <= i and
A4: i2 <= i by Def3;
A5: N . i in Y by A2, A4;
 N . i in X by A1, A3;
hence  X meets Y by A5, XBOOLE_0:3; ::_thesis: verum
end;

theorem Th18: :: YELLOW_6:18
for S being non empty 1-sorted
for N being net of S
for M being subnet of N
for X being set st M is_often_in X holds
N is_often_in X
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S
for M being subnet of N
for X being set st M is_often_in X holds
N is_often_in X
let N be net of S; ::_thesis: for M being subnet of N
for X being set st M is_often_in X holds
N is_often_in X
let M be subnet of N; ::_thesis: for X being set st M is_often_in X holds
N is_often_in X
let X be set ; ::_thesis: ( M is_often_in X implies N is_often_in X )
assume A1: M is_often_in X ; ::_thesis: N is_often_in X
let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of N st
( i <= b1 & N . b1 in X )
consider f being Function of M,N such that
A2: the mapping of M = the mapping of N * f and
A3: 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 Def9;
consider n being Element of M such that
A4: for p being Element of M st n <= p holds
i <= f . p by A3;
consider m being Element of M such that
A5: n <= m and
A6: M . m in X by A1, WAYBEL_0:def_12;
take  f . m ; ::_thesis: ( i <= f . m & N . (f . m) in X )
thus  i <= f . m by A4, A5; ::_thesis: N . (f . m) in X
thus  N . (f . m) in X by A2, A6, FUNCT_2:15; ::_thesis: verum
end;

theorem Th19: :: YELLOW_6:19
for S being non empty 1-sorted
for N being net of S
for X being set st N is_eventually_in X holds
N is_often_in X
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S
for X being set st N is_eventually_in X holds
N is_often_in X
let N be net of S; ::_thesis: for X being set st N is_eventually_in X holds
N is_often_in X
let X be set ; ::_thesis: ( N is_eventually_in X implies N is_often_in X )
given i being Element of N such that A1: for j being Element of N st i <= j holds
N . j in X ; :: according to WAYBEL_0:def_11 ::_thesis: N is_often_in X
let j be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of N st
( j <= b1 & N . b1 in X )
consider z being Element of N such that
A2: ( i <= z & j <= z ) by Def3;
take  z ; ::_thesis: ( j <= z & N . z in X )
thus  ( j <= z & N . z in X ) by A1, A2; ::_thesis: verum
end;

theorem Th20: :: YELLOW_6:20
for S being non empty 1-sorted
for N being net of S holds N is_eventually_in the carrier of S
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S holds N is_eventually_in the carrier of S
let N be net of S; ::_thesis: N is_eventually_in the carrier of S
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 the carrier of S )
let j be Element of N; ::_thesis: ( not the Element of N <= j or N . j in the carrier of S )
assume  the Element of N <= j ; ::_thesis: N . j in the carrier of S
thus  N . j in the carrier of S ; ::_thesis: verum
end;

begin

definition
let S be 1-sorted ;
let N be NetStr over S;
let X be set ;
funcN " X ->  strict SubNetStr of N means :Def10: :: YELLOW_6:def 10
( it is full SubRelStr of N & the carrier of it = the mapping of N " X );
existence
 ex b1 being strict SubNetStr of N st
( b1 is full SubRelStr of N & the carrier of b1 = the mapping of N " X )
proof
set c = the mapping of N " X;
reconsider i = the InternalRel of N |_2 ( the mapping of N " X) as Relation of ( the mapping of N " X),( the mapping of N " X) ;
percases ( not S is empty or S is empty ) ;
suppose not S is empty ; ::_thesis: ex b1 being strict SubNetStr of N st
( b1 is full SubRelStr of N & the carrier of b1 = the mapping of N " X )
then reconsider S = S as non empty 1-sorted ;
set c = the mapping of N " X;
reconsider m = the mapping of N | ( the mapping of N " X) as Function of ( the mapping of N " X), the carrier of S by FUNCT_2:32;
set S = NetStr(# ( the mapping of N " X),i,m #);
A1: i c= the InternalRel of N by XBOOLE_1:17;
then  NetStr(# ( the mapping of N " X),i,m #) is SubRelStr of N by YELLOW_0:def_13;
then reconsider S = NetStr(# ( the mapping of N " X),i,m #) as strict SubNetStr of N by Def6;
take  S ; ::_thesis: ( S is full SubRelStr of N & the carrier of S = the mapping of N " X )
thus  ( S is full SubRelStr of N & the carrier of S = the mapping of N " X ) by A1, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum
end;
supposeA2: S is empty ; ::_thesis: ex b1 being strict SubNetStr of N st
( b1 is full SubRelStr of N & the carrier of b1 = the mapping of N " X )
then  the mapping of N = {} ;
then  the mapping of N " X = {} ;
then reconsider m = {} as Function of ( the mapping of N " X), the carrier of S by RELSET_1:12;
set S = NetStr(# ( the mapping of N " X),i,m #);
A3: the mapping of NetStr(# ( the mapping of N " X),i,m #) = the mapping of N | the carrier of NetStr(# ( the mapping of N " X),i,m #) by A2;
A4: i c= the InternalRel of N by XBOOLE_1:17;
then  NetStr(# ( the mapping of N " X),i,m #) is SubRelStr of N by YELLOW_0:def_13;
then reconsider S = NetStr(# ( the mapping of N " X),i,m #) as strict SubNetStr of N by A3, Def6;
take  S ; ::_thesis: ( S is full SubRelStr of N & the carrier of S = the mapping of N " X )
thus  ( S is full SubRelStr of N & the carrier of S = the mapping of N " X ) by A4, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being strict SubNetStr of N st b1 is full SubRelStr of N & the carrier of b1 = the mapping of N " X & b2 is full SubRelStr of N & the carrier of b2 = the mapping of N " X holds
b1 = b2
proof
let it1, it2 be strict SubNetStr of N; ::_thesis: ( it1 is full SubRelStr of N & the carrier of it1 = the mapping of N " X & it2 is full SubRelStr of N & the carrier of it2 = the mapping of N " X implies it1 = it2 )
assume that
A5: it1 is full SubRelStr of N and
A6: the carrier of it1 = the mapping of N " X and
A7: it2 is full SubRelStr of N and
A8: the carrier of it2 = the mapping of N " X ; ::_thesis: it1 = it2
A9: the mapping of it1 = the mapping of N | the carrier of it2 by A6, A8, Def6
.= the mapping of it2 by Def6 ;
 RelStr(# the carrier of it1, the InternalRel of it1 #) = RelStr(# the carrier of it2, the InternalRel of it2 #) by A5, A6, A7, A8, YELLOW_0:57;
hence  it1 = it2 by A9; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines " YELLOW_6:def_10_:_
 for S being 1-sorted
for N being NetStr over S
for X being set
for b4 being strict SubNetStr of N holds
( b4 = N " X iff ( b4 is full SubRelStr of N & the carrier of b4 = the mapping of N " X ) );

registration
let S be 1-sorted ;
let N be transitive NetStr over S;
let X be set ;
clusterN " X ->  transitive strict full ;
coherence
 ( N " X is transitive & N " X is full )
proof
reconsider M = N " X as full SubRelStr of N by Def10;
 M is transitive ;
hence  ( N " X is transitive & N " X is full ) by Def7; ::_thesis: verum
end;
end;

theorem Th21: :: YELLOW_6:21
for S being non empty 1-sorted
for N being net of S
for X being set st N is_often_in X holds
( not N " X is empty & N " X is directed )
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S
for X being set st N is_often_in X holds
( not N " X is empty & N " X is directed )
let N be net of S; ::_thesis: for X being set st N is_often_in X holds
( not N " X is empty & N " X is directed )
let X be set ; ::_thesis: ( N is_often_in X implies ( not N " X is empty & N " X is directed ) )
assume A1: N is_often_in X ; ::_thesis: ( not N " X is empty & N " X is directed )
set i = the Element of N;
consider j being Element of N such that
 the Element of N <= j and
A2: N . j in X by A1, WAYBEL_0:def_12;
A3: j in the mapping of N " X by A2, FUNCT_2:38;
hence  not the carrier of (N " X) is empty by Def10; :: according to STRUCT_0:def_1 ::_thesis: N " X is directed
reconsider M = N " X as non empty full SubNetStr of N by A3, Def10;
 M is directed
proof
let i, j be Element of M; :: according to YELLOW_6:def_3 ::_thesis: ex z being Element of M st
( i <= z & j <= z )
A4: ( i in the carrier of M & j in the carrier of M ) ;
 the carrier of M c= the carrier of N by Th10;
then reconsider x = i, y = j as Element of N by A4;
consider z being Element of N such that
A5: ( x <= z & y <= z ) by Def3;
consider e being Element of N such that
A6: z <= e and
A7: N . e in X by A1, WAYBEL_0:def_12;
 e in the mapping of N " X by A7, FUNCT_2:38;
then reconsider k = e as Element of M by Def10;
take  k ; ::_thesis: ( i <= k & j <= k )
 ( x <= e & y <= e ) by A5, A6, YELLOW_0:def_2;
hence  ( i <= k & j <= k ) by Th12; ::_thesis: verum
end;
hence  N " X is directed ; ::_thesis: verum
end;

theorem Th22: :: YELLOW_6:22
for S being non empty 1-sorted
for N being net of S
for X being set st N is_often_in X holds
N " X is subnet of N
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S
for X being set st N is_often_in X holds
N " X is subnet of N
let N be net of S; ::_thesis: for X being set st N is_often_in X holds
N " X is subnet of N
let X be set ; ::_thesis: ( N is_often_in X implies N " X is subnet of N )
assume A1: N is_often_in X ; ::_thesis: N " X is subnet of N
then reconsider M = N " X as net of S by Th21;
 M is subnet of N
proof
set f = id M;
 the carrier of M c= the carrier of N by Th10;
then reconsider f = id M as Function of M,N by FUNCT_2:7;
take  f ; :: according to YELLOW_6:def_9 ::_thesis: ( 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 ) )
 the mapping of M = the mapping of N | the carrier of M by Def6;
hence  the mapping of M = the mapping of N * f by RELAT_1:65; ::_thesis: 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
let m be Element of N; ::_thesis: ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p
consider j being Element of N such that
A2: m <= j and
A3: N . j in X by A1, WAYBEL_0:def_12;
 j in the mapping of N " X by A3, FUNCT_2:38;
then reconsider n = j as Element of M by Def10;
take  n ; ::_thesis: for p being Element of M st n <= p holds
m <= f . p
let p be Element of M; ::_thesis: ( n <= p implies m <= f . p )
assume A4: n <= p ; ::_thesis: m <= f . p
 f . p = p by FUNCT_1:18;
then  j <= f . p by A4, Th11;
hence  m <= f . p by A2, YELLOW_0:def_2; ::_thesis: verum
end;
hence  N " X is subnet of N ; ::_thesis: verum
end;

theorem Th23: :: YELLOW_6:23
for S being non empty 1-sorted
for N being net of S
for X being set
for M being subnet of N st M = N " X holds
M is_eventually_in X
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S
for X being set
for M being subnet of N st M = N " X holds
M is_eventually_in X
let N be net of S; ::_thesis: for X being set
for M being subnet of N st M = N " X holds
M is_eventually_in X
let X be set ; ::_thesis: for M being subnet of N st M = N " X holds
M is_eventually_in X
let M be subnet of N; ::_thesis: ( M = N " X implies M is_eventually_in X )
assume A1: M = N " X ; ::_thesis: M is_eventually_in X
set i = the Element of M;
take  the Element of M ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of M holds
( not the Element of M <= b1 or M . b1 in X )
let j be Element of M; ::_thesis: ( not the Element of M <= j or M . j in X )
assume  the Element of M <= j ; ::_thesis: M . j in X
 j in the carrier of M ;
then  j in the mapping of N " X by A1, Def10;
then A2: the mapping of N . j in X by FUNCT_1:def_7;
 the mapping of M = the mapping of N | the carrier of M by A1, Def6;
hence  M . j in X by A2, FUNCT_1:49; ::_thesis: verum
end;

begin

definition
let X be non empty 1-sorted ;
func NetUniv X ->  set  means :Def11: :: YELLOW_6:def 11
 for x being set holds
( x in it iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) )
proof
deffunc H1( set ) ->  set =  {  NetStr(# $1,r,f #) where r is Relation of $1,$1, f is Element of Funcs ($1, the carrier of X) : NetStr(# $1,r,f #) is net of X  }  ;
set I = the_universe_of the carrier of X;
consider M being ManySortedSet of the_universe_of the carrier of X such that
A1: for i being set st i in the_universe_of the carrier of X holds
M . i = H1(i) from PBOOLE:sch_4();
take IT = Union M; ::_thesis: for x being set holds
( x in IT iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) )
let x be set ; ::_thesis: ( x in IT iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) )
A2: Union M = union (rng M) by CARD_3:def_4;
hereby  ::_thesis: ( ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) implies x in IT )
assume  x in IT ; ::_thesis: ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X )
then consider y being set  such that
A3: x in y and
A4: y in rng M by A2, TARSKI:def_4;
consider z being set  such that
A5: z in dom M and
A6: M . z = y by A4, FUNCT_1:def_3;
 z in the_universe_of the carrier of X by A5;
then  y =  {  NetStr(# z,r,f #) where r is Relation of z,z, f is Element of Funcs (z, the carrier of X) : NetStr(# z,r,f #) is net of X  }  by A1, A6;
then consider r being Relation of z,z, f being Element of Funcs (z, the carrier of X) such that
A7: x = NetStr(# z,r,f #) and
A8: NetStr(# z,r,f #) is net of X by A3;
reconsider N = NetStr(# z,r,f #) as strict net of X by A8;
take N = N; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of X )
thus  N = x by A7; ::_thesis: the carrier of N in the_universe_of the carrier of X
thus  the carrier of N in the_universe_of the carrier of X by A5; ::_thesis: verum
end;
given N being strict net of X such that A9: N = x and
A10: the carrier of N in the_universe_of the carrier of X ; ::_thesis: x in IT
set i = the carrier of N;
 the carrier of N in dom M by A10, PARTFUN1:def_2;
then A11: M . the carrier of N in rng M by FUNCT_1:def_3;
A12: the mapping of N in Funcs ( the carrier of N, the carrier of X) by FUNCT_2:8;
 M . the carrier of N =  {  NetStr(# the carrier of N,r,f #) where r is Relation of the carrier of N, the carrier of N, f is Element of Funcs ( the carrier of N, the carrier of X) : NetStr(# the carrier of N,r,f #) is net of X  }  by A1, A10;
then  N in M . the carrier of N by A12;
hence  x in IT by A2, A9, A11, TARSKI:def_4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) ) ) & ( for x being set holds
( x in b2 iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex N being strict net of X st
( N = $1 & the carrier of N in the_universe_of the carrier of X );
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def11 defines NetUniv YELLOW_6:def_11_:_
 for X being non empty 1-sorted
for b2 being set holds
( b2 = NetUniv X iff for x being set holds
( x in b2 iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) ) );

registration
let X be non empty 1-sorted ;
cluster NetUniv X ->  non empty ;
coherence
 not NetUniv X is empty
proof
 {} in {{}} by TARSKI:def_1;
then reconsider r = {[{},{}]} as Relation of {{}} by RELSET_1:3;
set R = RelStr(# {{}},r #);
A1: now__::_thesis:_for_x,_y_being_Element_of_RelStr(#_{{}},r_#)_holds_x_<=_y
let x, y be Element of RelStr(# {{}},r #); ::_thesis: x <= y
 ( x = {} & y = {} ) by TARSKI:def_1;
then  [x,y] in {[{},{}]} by TARSKI:def_1;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
A2: RelStr(# {{}},r #) is transitive
proof
let x, y, z be Element of RelStr(# {{}},r #); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
thus  ( not x <= y or not y <= z or x <= z ) by A1; ::_thesis: verum
end;
 RelStr(# {{}},r #) is directed
proof
let x, y be Element of RelStr(# {{}},r #); :: according to YELLOW_6:def_3 ::_thesis: ex z being Element of RelStr(# {{}},r #) st
( x <= z & y <= z )
take  x ; ::_thesis: ( x <= x & y <= x )
thus  ( x <= x & y <= x ) by A1; ::_thesis: verum
end;
then reconsider R = RelStr(# {{}},r #) as non empty transitive directed RelStr by A2;
set V = the_universe_of the carrier of X;
set q = the Element of X;
set N = ConstantNet (R, the Element of X);
 ( RelStr(# the carrier of (ConstantNet (R, the Element of X)), the InternalRel of (ConstantNet (R, the Element of X)) #) = RelStr(# the carrier of R, the InternalRel of R #) & {} in the_universe_of the carrier of X ) by Def5, CLASSES2:56;
then  the carrier of (ConstantNet (R, the Element of X)) in the_universe_of the carrier of X by CLASSES2:2;
hence  not NetUniv X is empty by Def11; ::_thesis: verum
end;
end;

Lm6:  for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
for N being constant net of S1 holds N is constant net of S2
proof
let S1, S2 be non empty 1-sorted ; ::_thesis: ( the carrier of S1 = the carrier of S2 implies for N being constant net of S1 holds N is constant net of S2 )
assume A1: the carrier of S1 = the carrier of S2 ; ::_thesis: for N being constant net of S1 holds N is constant net of S2
let N be constant net of S1; ::_thesis: N is constant net of S2
reconsider M = N as net of S2 by A1;
 the mapping of N is constant ;
then  the mapping of M is constant ;
hence  N is constant net of S2 by Def4; ::_thesis: verum
end;

Lm7:  for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
proof
let S1, S2 be non empty 1-sorted ; ::_thesis: ( the carrier of S1 = the carrier of S2 implies NetUniv S1 = NetUniv S2 )
defpred S1[ set ] means  ex N being strict net of S2 st
( N = $1 & the carrier of N in the_universe_of the carrier of S2 );
assume A1: the carrier of S1 = the carrier of S2 ; ::_thesis: NetUniv S1 = NetUniv S2
A2: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_NetUniv_S1_implies_S1[x]_)_&_(_S1[x]_implies_x_in_NetUniv_S1_)_)
let x be set ; ::_thesis: ( ( x in NetUniv S1 implies S1[x] ) & ( S1[x] implies x in NetUniv S1 ) )
hereby  ::_thesis: ( S1[x] implies x in NetUniv S1 )
assume  x in NetUniv S1 ; ::_thesis: S1[x]
then consider N being strict net of S1 such that
A3: ( N = x & the carrier of N in the_universe_of the carrier of S1 ) by Def11;
reconsider N = N as strict net of S2 by A1;
thus  S1[x] ::_thesis: verum
proof
take  N ; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of S2 )
thus  ( N = x & the carrier of N in the_universe_of the carrier of S2 ) by A1, A3; ::_thesis: verum
end;
end;
assume  S1[x] ; ::_thesis: x in NetUniv S1
then consider N being strict net of S2 such that
A4: ( N = x & the carrier of N in the_universe_of the carrier of S2 ) ;
reconsider N = N as strict net of S1 by A1;
now__::_thesis:_ex_N_being_strict_net_of_S1_st_
(_N_=_x_&_the_carrier_of_N_in_the_universe_of_the_carrier_of_S1_)
take N = N; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of S1 )
thus  ( N = x & the carrier of N in the_universe_of the carrier of S1 ) by A1, A4; ::_thesis: verum
end;
hence  x in NetUniv S1 by Def11; ::_thesis: verum
end;
A5: for x being set holds
( x in NetUniv S2 iff S1[x] ) by Def11;
thus  NetUniv S1 = NetUniv S2 from XBOOLE_0:sch_2(A2, A5); ::_thesis: verum
end;

begin

definition
let X be set ;
let T be 1-sorted ;
mode net_set of X,T ->  ManySortedSet of X means :Def12: :: YELLOW_6:def 12
 for i being set st i in rng it holds
i is net of T;
existence
 ex b1 being ManySortedSet of X st
for i being set st i in rng b1 holds
i is net of T
proof
set N = the net of T;
take  X --> the net of T ; ::_thesis: for i being set st i in rng (X --> the net of T) holds
i is net of T
let i be set ; ::_thesis: ( i in rng (X --> the net of T) implies i is net of T )
assume  i in rng (X --> the net of T) ; ::_thesis: i is net of T
hence  i is net of T by TARSKI:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines net_set YELLOW_6:def_12_:_
 for X being set
for T being 1-sorted
for b3 being ManySortedSet of X holds
( b3 is net_set of X,T iff for i being set st i in rng b3 holds
i is net of T );

theorem Th24: :: YELLOW_6:24
for X being set
for T being 1-sorted
for F being ManySortedSet of X holds
( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )
proof
let X be set ; ::_thesis: for T being 1-sorted
for F being ManySortedSet of X holds
( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )
let T be 1-sorted ; ::_thesis: for F being ManySortedSet of X holds
( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )
let F be ManySortedSet of X; ::_thesis: ( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )
hereby  ::_thesis: ( ( for i being set st i in X holds
F . i is net of T ) implies F is net_set of X,T )
assume A1: F is net_set of X,T ; ::_thesis: for i being set st i in X holds
F . i is net of T
let i be set ; ::_thesis: ( i in X implies F . i is net of T )
assume  i in X ; ::_thesis: F . i is net of T
then  i in dom F by PARTFUN1:def_2;
then  F . i in rng F by FUNCT_1:def_3;
hence  F . i is net of T by A1, Def12; ::_thesis: verum
end;
assume A2: for i being set st i in X holds
F . i is net of T ; ::_thesis: F is net_set of X,T
let x be set ; :: according to YELLOW_6:def_12 ::_thesis: ( x in rng F implies x is net of T )
assume  x in rng F ; ::_thesis: x is net of T
then  ex i being set st
( i in dom F & x = F . i ) by FUNCT_1:def_3;
hence  x is net of T by A2; ::_thesis: verum
end;

definition
let X be non empty set ;
let T be 1-sorted ;
let J be net_set of X,T;
let i be Element of X;
:: original: .
redefine funcJ . i ->  net of T;
coherence
 J . i is net of T by Th24;
end;

registration
let X be set ;
let T be 1-sorted ;
cluster  ->  RelStr-yielding for net_set of X,T;
coherence
 for b1 being net_set of X,T holds b1 is RelStr-yielding
proof
let F be net_set of X,T; ::_thesis: F is RelStr-yielding
let v be set ; :: according to YELLOW_1:def_3 ::_thesis: ( not v in proj2 F or v is RelStr )
assume  v in rng F ; ::_thesis: v is RelStr
hence  v is RelStr by Def12; ::_thesis: verum
end;
end;

registration
let T be 1-sorted ;
let Y be net of T;
cluster  ->  yielding_non-empty_carriers for net_set of the carrier of Y,T;
coherence
 for b1 being net_set of the carrier of Y,T holds b1 is yielding_non-empty_carriers
proof
let J be net_set of the carrier of Y,T; ::_thesis: J is yielding_non-empty_carriers
let i be set ; :: according to YELLOW_6:def_2 ::_thesis: ( i in rng J implies i is non empty 1-sorted )
assume  i in rng J ; ::_thesis: i is non empty 1-sorted
hence  i is non empty 1-sorted by Def12; ::_thesis: verum
end;
end;

registration
let T be non empty 1-sorted ;
let Y be net of T;
let J be net_set of the carrier of Y,T;
cluster product J ->  transitive directed ;
coherence
 ( product J is directed & product J is transitive )
proof
A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def_4;
thus  product J is directed ::_thesis: product J is transitive
proof
let x, y be Element of (product J); :: according to YELLOW_6:def_3 ::_thesis: ex z being Element of (product J) st
( x <= z & y <= z )
defpred S1[ Element of Y, set ] means ( [(x . T),Y] in the InternalRel of (J . T) & [(y . T),Y] in the InternalRel of (J . T) );
A2: now__::_thesis:_for_i_being_Element_of_Y_ex_z_being_set_st_S1[i,z]
let i be Element of Y; ::_thesis: ex z being set st S1[i,z]
consider zi being Element of (J . i) such that
A3: ( x . i <= zi & y . i <= zi ) by Def3;
reconsider z = zi as set ;
take z = z; ::_thesis: S1[i,z]
thus  S1[i,z] by A3, ORDERS_2:def_5; ::_thesis: verum
end;
consider z being ManySortedSet of the carrier of Y such that
A4: for i being Element of Y holds S1[i,z . i] from PBOOLE:sch_6(A2);
A5: now__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_J)_holds_
z_._i_in_(Carrier_J)_._i
let i be set ; ::_thesis: ( i in dom (Carrier J) implies z . i in (Carrier J) . i )
assume  i in dom (Carrier J) ; ::_thesis: z . i in (Carrier J) . i
then reconsider j = i as Element of Y ;
 [(x . j),(z . j)] in the InternalRel of (J . j) by A4;
then  z . j in the carrier of (J . j) by ZFMISC_1:87;
hence  z . i in (Carrier J) . i by Th2; ::_thesis: verum
end;
dom z = the carrier of Y by PARTFUN1:def_2
.= dom (Carrier J) by PARTFUN1:def_2 ;
then reconsider z = z as Element of (product J) by A1, A5, CARD_3:9;
take  z ; ::_thesis: ( x <= z & y <= z )
 for i being set st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
proof
let i be set ; ::_thesis: ( i in the carrier of Y implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi ) )
assume  i in the carrier of Y ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
then reconsider j = i as Element of Y ;
reconsider xi = x . j, zi = z . j as Element of (J . j) ;
take  J . j ; ::_thesis: ex xi, yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take  zi ; ::_thesis: ( J . j = J . i & xi = x . i & zi = z . i & xi <= zi )
thus  ( J . j = J . i & xi = x . i & zi = z . i ) ; ::_thesis: xi <= zi
 [xi,zi] in the InternalRel of (J . j) by A4;
hence  xi <= zi by ORDERS_2:def_5; ::_thesis: verum
end;
hence  x <= z by A1, YELLOW_1:def_4; ::_thesis: y <= z
 for i being set st i in the carrier of Y holds
ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi )
proof
let i be set ; ::_thesis: ( i in the carrier of Y implies ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi ) )
assume  i in the carrier of Y ; ::_thesis: ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi )
then reconsider j = i as Element of Y ;
reconsider yi = y . j, zi = z . j as Element of (J . j) ;
take  J . j ; ::_thesis: ex yi, zi being Element of (J . j) st
( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
take  yi ; ::_thesis: ex zi being Element of (J . j) st
( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
take  zi ; ::_thesis: ( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
thus  ( J . j = J . i & yi = y . i & zi = z . i ) ; ::_thesis: yi <= zi
 [yi,zi] in the InternalRel of (J . j) by A4;
hence  yi <= zi by ORDERS_2:def_5; ::_thesis: verum
end;
hence  y <= z by A1, YELLOW_1:def_4; ::_thesis: verum
end;
let x, y, z be Element of (product J); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A6: x <= y and
A7: y <= z ; ::_thesis: x <= z
A8: ex fy, gz being Function st
( fy = y & gz = z & ( for i being set st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = fy . i & yi = gz . i & xi <= yi ) ) ) by A1, A7, YELLOW_1:def_4;
A9: ex fx, gy being Function st
( fx = x & gy = y & ( for i being set st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = fx . i & yi = gy . i & xi <= yi ) ) ) by A1, A6, YELLOW_1:def_4;
 for i being set st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
proof
let i be set ; ::_thesis: ( i in the carrier of Y implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi ) )
assume A10: i in the carrier of Y ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
then reconsider j = i as Element of Y ;
consider R1 being RelStr , xi, yi being Element of R1 such that
A11: R1 = J . i and
A12: xi = x . i and
A13: ( yi = y . i & xi <= yi ) by A9, A10;
consider R2 being RelStr , yi9, zi being Element of R2 such that
A14: R2 = J . i and
A15: yi9 = y . i and
A16: zi = z . i and
A17: yi9 <= zi by A8, A10;
reconsider xi = xi, zi = zi as Element of (J . j) by A11, A14;
take  J . j ; ::_thesis: ex xi, yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take  zi ; ::_thesis: ( J . j = J . i & xi = x . i & zi = z . i & xi <= zi )
thus  ( J . j = J . i & xi = x . i & zi = z . i ) by A12, A16; ::_thesis: xi <= zi
thus  xi <= zi by A11, A13, A14, A15, A17, YELLOW_0:def_2; ::_thesis: verum
end;
hence  x <= z by A1, YELLOW_1:def_4; ::_thesis: verum
end;
end;

registration
let X be set ;
let T be 1-sorted ;
cluster  ->  yielding_non-empty_carriers for net_set of X,T;
coherence
 for b1 being net_set of X,T holds b1 is yielding_non-empty_carriers
proof
let F be net_set of X,T; ::_thesis: F is yielding_non-empty_carriers
let v be set ; :: according to YELLOW_6:def_2 ::_thesis: ( v in rng F implies v is non empty 1-sorted )
assume  v in rng F ; ::_thesis: v is non empty 1-sorted
hence  v is non empty 1-sorted by Def12; ::_thesis: verum
end;
end;

registration
let X be set ;
let T be 1-sorted ;
cluster Relation-like X -defined Function-like V14(X) 1-sorted-yielding RelStr-yielding yielding_non-empty_carriers for net_set of X,T;
existence
 ex b1 being net_set of X,T st b1 is yielding_non-empty_carriers
proof
set F = the net_set of X,T;
take  the net_set of X,T ; ::_thesis: the net_set of X,T is yielding_non-empty_carriers
thus  the net_set of X,T is yielding_non-empty_carriers ; ::_thesis: verum
end;
end;

definition
let T be non empty 1-sorted ;
let Y be net of T;
let J be net_set of the carrier of Y,T;
func Iterated J ->  strict net of T means :Def13: :: YELLOW_6:def 13
( RelStr(# the carrier of it, the InternalRel of it #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of it . (i,f) = the mapping of (J . i) . (f . i) ) );
existence
 ex b1 being strict net of T st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b1 . (i,f) = the mapping of (J . i) . (f . i) ) )
proof
deffunc H1( Element of Y, Element of (product J)) ->  Element of the carrier of T = the mapping of (J . $1) . ($2 . $1);
set R = [:Y,(product J):];
A1: for i being Element of Y
for f being Element of (product J) holds H1(i,f) in the carrier of T ;
consider F being Function of [: the carrier of Y, the carrier of (product J):], the carrier of T such that
A2: for i being Element of Y
for f being Element of (product J) holds F . (i,f) = H1(i,f) from FUNCT_7:sch_1(A1);
 the carrier of [:Y,(product J):] = [: the carrier of Y, the carrier of (product J):] by YELLOW_3:def_2;
then reconsider F = F as Function of the carrier of [:Y,(product J):], the carrier of T ;
reconsider N = NetStr(# the carrier of [:Y,(product J):], the InternalRel of [:Y,(product J):],F #) as strict net of T by Lm1, Lm2;
take  N ; ::_thesis: ( RelStr(# the carrier of N, the InternalRel of N #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of N . (i,f) = the mapping of (J . i) . (f . i) ) )
thus  RelStr(# the carrier of N, the InternalRel of N #) = [:Y,(product J):] ; ::_thesis: for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of N . (i,f) = the mapping of (J . i) . (f . i)
let i be Element of Y; ::_thesis: for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of N . (i,f) = the mapping of (J . i) . (f . i)
let f be Function; ::_thesis: ( i in the carrier of Y & f in the carrier of (product J) implies the mapping of N . (i,f) = the mapping of (J . i) . (f . i) )
assume that
 i in the carrier of Y and
A3: f in the carrier of (product J) ; ::_thesis: the mapping of N . (i,f) = the mapping of (J . i) . (f . i)
thus  the mapping of N . (i,f) = the mapping of (J . i) . (f . i) by A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict net of T st RelStr(# the carrier of b1, the InternalRel of b1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b1 . (i,f) = the mapping of (J . i) . (f . i) ) & RelStr(# the carrier of b2, the InternalRel of b2 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b2 . (i,f) = the mapping of (J . i) . (f . i) ) holds
b1 = b2
proof
let IT1, IT2 be strict net of T; ::_thesis: ( RelStr(# the carrier of IT1, the InternalRel of IT1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of IT1 . (i,f) = the mapping of (J . i) . (f . i) ) & RelStr(# the carrier of IT2, the InternalRel of IT2 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of IT2 . (i,f) = the mapping of (J . i) . (f . i) ) implies IT1 = IT2 )
assume that
A4: RelStr(# the carrier of IT1, the InternalRel of IT1 #) = [:Y,(product J):] and
A5: for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of IT1 . (i,f) = the mapping of (J . i) . (f . i) and
A6: RelStr(# the carrier of IT2, the InternalRel of IT2 #) = [:Y,(product J):] and
A7: for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of IT2 . (i,f) = the mapping of (J . i) . (f . i) ; ::_thesis: IT1 = IT2
 the carrier of RelStr(# the carrier of IT2, the InternalRel of IT2 #) = [: the carrier of Y, the carrier of (product J):] by A6, YELLOW_3:def_2;
then reconsider m1 = the mapping of IT1, m2 = the mapping of IT2 as Function of [: the carrier of Y, the carrier of (product J):], the carrier of T by A4, A6;
now__::_thesis:_for_c_being_Element_of_[:_the_carrier_of_Y,_the_carrier_of_(product_J):]_holds_m1_._c_=_m2_._c
let c be Element of [: the carrier of Y, the carrier of (product J):]; ::_thesis: m1 . c = m2 . c
consider c1 being Element of Y, c2 being Element of (product J) such that
A8: c = [c1,c2] by DOMAIN_1:1;
reconsider d = c2 as Element of product (Carrier J) by YELLOW_1:def_4;
thus m1 . c = m1 . (c1,d) by A8
.= the mapping of (J . c1) . (d . c1) by A5
.= m2 . (c1,d) by A7
.= m2 . c by A8 ; ::_thesis: verum
end;
hence  IT1 = IT2 by A4, A6, FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines Iterated YELLOW_6:def_13_:_
 for T being non empty 1-sorted
for Y being net of T
for J being net_set of the carrier of Y,T
for b4 being strict net of T holds
( b4 = Iterated J iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b4 . (i,f) = the mapping of (J . i) . (f . i) ) ) );

theorem Th25: :: YELLOW_6:25
for T being non empty 1-sorted
for Y being net of T
for J being net_set of the carrier of Y,T st Y in NetUniv T & ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T
proof
let T be non empty 1-sorted ; ::_thesis: for Y being net of T
for J being net_set of the carrier of Y,T st Y in NetUniv T & ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T
let Y be net of T; ::_thesis: for J being net_set of the carrier of Y,T st Y in NetUniv T & ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T
let J be net_set of the carrier of Y,T; ::_thesis: ( Y in NetUniv T & ( for i being Element of Y holds J . i in NetUniv T ) implies Iterated J in NetUniv T )
assume that
A1: Y in NetUniv T and
A2: for i being Element of Y holds J . i in NetUniv T ; ::_thesis: Iterated J in NetUniv T
A3: rng (Carrier J) c= the_universe_of the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Carrier J) or x in the_universe_of the carrier of T )
assume  x in rng (Carrier J) ; ::_thesis: x in the_universe_of the carrier of T
then consider y being set  such that
A4: y in dom (Carrier J) and
A5: (Carrier J) . y = x by FUNCT_1:def_3;
reconsider i = y as Element of Y by A4;
 J . i in NetUniv T by A2;
then  ex N being strict net of T st
( N = J . i & the carrier of N in the_universe_of the carrier of T ) by Def11;
hence  x in the_universe_of the carrier of T by A5, Th2; ::_thesis: verum
end;
 RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = [:Y,(product J):] by Def13;
then A6: the carrier of (Iterated J) = [: the carrier of Y, the carrier of (product J):] by YELLOW_3:def_2;
A7: ex N being strict net of T st
( N = Y & the carrier of N in the_universe_of the carrier of T ) by A1, Def11;
then  dom (Carrier J) in the_universe_of the carrier of T by PARTFUN1:def_2;
then  product (Carrier J) in the_universe_of the carrier of T by A3, Th1;
then  the carrier of (product J) in the_universe_of the carrier of T by YELLOW_1:def_4;
then  the carrier of (Iterated J) in the_universe_of the carrier of T by A6, A7, CLASSES2:61;
hence  Iterated J in NetUniv T by Def11; ::_thesis: verum
end;

theorem Th26: :: YELLOW_6:26
for T being non empty 1-sorted
for N being net of T
for J being net_set of the carrier of N,T holds the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]
proof
let T be non empty 1-sorted ; ::_thesis: for N being net of T
for J being net_set of the carrier of N,T holds the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]
let N be net of T; ::_thesis: for J being net_set of the carrier of N,T holds the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]
let J be net_set of the carrier of N,T; ::_thesis: the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]
 RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = [:N,(product J):] by Def13;
hence  the carrier of (Iterated J) = [: the carrier of N, the carrier of (product J):] by YELLOW_3:def_2
.= [: the carrier of N,(product (Carrier J)):] by YELLOW_1:def_4 ;
::_thesis: verum
end;

theorem Th27: :: YELLOW_6:27
for T being non empty 1-sorted
for N being net of T
for J being net_set of the carrier of N,T
for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
proof
let T be non empty 1-sorted ; ::_thesis: for N being net of T
for J being net_set of the carrier of N,T
for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let N be net of T; ::_thesis: for J being net_set of the carrier of N,T
for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let J be net_set of the carrier of N,T; ::_thesis: for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let i be Element of N; ::_thesis: for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let f be Element of (product J); ::_thesis: for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
let x be Element of (Iterated J); ::_thesis: ( x = [i,f] implies (Iterated J) . x = the mapping of (J . i) . (f . i) )
assume  x = [i,f] ; ::_thesis: (Iterated J) . x = the mapping of (J . i) . (f . i)
hence (Iterated J) . x = the mapping of (Iterated J) . (i,f)
.= the mapping of (J . i) . (f . i) by Def13 ;
::_thesis: verum
end;

theorem Th28: :: YELLOW_6:28
for T being non empty 1-sorted
for Y being net of T
for J being net_set of the carrier of Y,T holds rng the mapping of (Iterated J) c= union  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }
proof
let T be non empty 1-sorted ; ::_thesis: for Y being net of T
for J being net_set of the carrier of Y,T holds rng the mapping of (Iterated J) c= union  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }
let Y be net of T; ::_thesis: for J being net_set of the carrier of Y,T holds rng the mapping of (Iterated J) c= union  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }
let J be net_set of the carrier of Y,T; ::_thesis: rng the mapping of (Iterated J) c= union  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the mapping of (Iterated J) or x in union  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }  )
set X =  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }  ;
assume  x in rng the mapping of (Iterated J) ; ::_thesis: x in union  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }
then consider y being set  such that
A1: y in dom the mapping of (Iterated J) and
A2: the mapping of (Iterated J) . y = x by FUNCT_1:def_3;
 y in the carrier of (Iterated J) by A1;
then  y in [: the carrier of Y,(product (Carrier J)):] by Th26;
then consider y1 being Element of Y, y2 being Element of product (Carrier J) such that
A3: y = [y1,y2] by DOMAIN_1:1;
 y1 in the carrier of Y ;
then  y1 in dom (Carrier J) by PARTFUN1:def_2;
then  y2 . y1 in (Carrier J) . y1 by CARD_3:9;
then  y2 . y1 in the carrier of (J . y1) by Th2;
then A4: y2 . y1 in dom the mapping of (J . y1) by FUNCT_2:def_1;
 y2 in product (Carrier J) ;
then A5: y2 in the carrier of (product J) by YELLOW_1:def_4;
x = the mapping of (Iterated J) . (y1,y2) by A2, A3
.= the mapping of (J . y1) . (y2 . y1) by A5, Def13 ;
then A6: x in rng the mapping of (J . y1) by A4, FUNCT_1:def_3;
reconsider y1 = y1 as Element of Y ;
 rng the mapping of (J . y1) in  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }  ;
hence  x in union  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }  by A6, TARSKI:def_4; ::_thesis: verum
end;

begin

definition
let T be non empty TopSpace;
let p be Point of T;
func OpenNeighborhoods p ->  RelStr  equals :: YELLOW_6:def 14
(InclPoset  {  V where V is Subset of T : ( p in V & V is open )  }  ) ~ ;
correctness
coherence
(InclPoset  {  V where V is Subset of T : ( p in V & V is open )  }  ) ~ is RelStr ;
;
end;

:: deftheorem  defines OpenNeighborhoods YELLOW_6:def_14_:_
 for T being non empty TopSpace
for p being Point of T holds OpenNeighborhoods p = (InclPoset  {  V where V is Subset of T : ( p in V & V is open )  }  ) ~ ;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster OpenNeighborhoods p ->  non empty ;
coherence
 not OpenNeighborhoods p is empty
proof
set Xp =  {  v where v is Subset of T : ( p in v & v is open )  }  ;
 [#] T in the carrier of (InclPoset  {  v where v is Subset of T : ( p in v & v is open )  }  ) ;
hence  not the carrier of (OpenNeighborhoods p) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem Th29: :: YELLOW_6:29
for T being non empty TopSpace
for p being Point of T
for x being Element of (OpenNeighborhoods p) ex W being Subset of T st
( W = x & p in W & W is open )
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T
for x being Element of (OpenNeighborhoods p) ex W being Subset of T st
( W = x & p in W & W is open )
let p be Point of T; ::_thesis: for x being Element of (OpenNeighborhoods p) ex W being Subset of T st
( W = x & p in W & W is open )
let x be Element of (OpenNeighborhoods p); ::_thesis: ex W being Subset of T st
( W = x & p in W & W is open )
set X =  {  V where V is Subset of T : ( p in V & V is open )  }  ;
 x in the carrier of ((InclPoset  {  V where V is Subset of T : ( p in V & V is open )  }  ) ~) ;
then  x in the carrier of (InclPoset  {  V where V is Subset of T : ( p in V & V is open )  }  ) by Th3;
hence  ex W being Subset of T st
( W = x & p in W & W is open ) ; ::_thesis: verum
end;

theorem Th30: :: YELLOW_6:30
for T being non empty TopSpace
for p being Point of T
for x being Subset of T holds
( x in the carrier of (OpenNeighborhoods p) iff ( p in x & x is open ) )
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T
for x being Subset of T holds
( x in the carrier of (OpenNeighborhoods p) iff ( p in x & x is open ) )
let p be Point of T; ::_thesis: for x being Subset of T holds
( x in the carrier of (OpenNeighborhoods p) iff ( p in x & x is open ) )
let x be Subset of T; ::_thesis: ( x in the carrier of (OpenNeighborhoods p) iff ( p in x & x is open ) )
set Xp =  {  v where v is Subset of T : ( p in v & v is open )  }  ;
reconsider i = x as Subset of T ;
thus  ( x in the carrier of (OpenNeighborhoods p) implies ( p in x & x is open ) ) ::_thesis: ( p in x & x is open implies x in the carrier of (OpenNeighborhoods p) )
proof
assume  x in the carrier of (OpenNeighborhoods p) ; ::_thesis: ( p in x & x is open )
then  ex v being Subset of T st
( i = v & p in v & v is open ) by Th29;
hence  ( p in x & x is open ) ; ::_thesis: verum
end;
assume  ( p in x & x is open ) ; ::_thesis: x in the carrier of (OpenNeighborhoods p)
then  x in the carrier of (InclPoset  {  v where v is Subset of T : ( p in v & v is open )  }  ) ;
hence  x in the carrier of (OpenNeighborhoods p) by Th3; ::_thesis: verum
end;

theorem Th31: :: YELLOW_6:31
for T being non empty TopSpace
for p being Point of T
for x, y being Element of (OpenNeighborhoods p) holds
( x <= y iff y c= x )
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T
for x, y being Element of (OpenNeighborhoods p) holds
( x <= y iff y c= x )
let p be Point of T; ::_thesis: for x, y being Element of (OpenNeighborhoods p) holds
( x <= y iff y c= x )
set X =  {  V where V is Subset of T : ( p in V & V is open )  }  ;
 [#] T in  {  V where V is Subset of T : ( p in V & V is open )  }  ;
then reconsider X =  {  V where V is Subset of T : ( p in V & V is open )  }  as non empty set ;
let x, y be Element of (OpenNeighborhoods p); ::_thesis: ( x <= y iff y c= x )
 (InclPoset X) ~ = RelStr(# the carrier of (InclPoset X),( the InternalRel of (InclPoset X) ~) #) by LATTICE3:def_5;
then reconsider a = x, b = y as Element of (InclPoset X) ;
A1: ( b <= a iff y c= x ) by YELLOW_1:3;
 ( x = a ~ & y = b ~ ) by LATTICE3:def_6;
hence  ( x <= y iff y c= x ) by A1, LATTICE3:9; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster OpenNeighborhoods p ->  transitive directed ;
coherence
 ( OpenNeighborhoods p is transitive & OpenNeighborhoods p is directed )
proof
thus  OpenNeighborhoods p is transitive ; ::_thesis: OpenNeighborhoods p is directed
let x, y be Element of (OpenNeighborhoods p); :: according to YELLOW_6:def_3 ::_thesis: ex z being Element of (OpenNeighborhoods p) st
( x <= z & y <= z )
set X =  {  V where V is Subset of T : ( p in V & V is open )  }  ;
consider V being Subset of T such that
A1: x = V and
A2: ( p in V & V is open ) by Th29;
consider W being Subset of T such that
A3: y = W and
A4: ( p in W & W is open ) by Th29;
set z = V /\ W;
 ( p in V /\ W & V /\ W is open ) by A2, A4, XBOOLE_0:def_4;
then  V /\ W in  {  V where V is Subset of T : ( p in V & V is open )  }  ;
then reconsider z = V /\ W as Element of (OpenNeighborhoods p) by Th3;
A5: z c= y by A3, XBOOLE_1:17;
take  z ; ::_thesis: ( x <= z & y <= z )
 z c= x by A1, XBOOLE_1:17;
hence  ( x <= z & y <= z ) by A5, Th31; ::_thesis: verum
end;
end;

begin

definition
let T be non empty TopSpace;
let N be net of T;
defpred S1[ Point of T] means  for V being a_neighborhood of $1 holds N is_eventually_in V;
func Lim N ->  Subset of T means :Def15: :: YELLOW_6:def 15
 for p being Point of T holds
( p in it iff for V being a_neighborhood of p holds N is_eventually_in V );
existence
 ex b1 being Subset of T st
for p being Point of T holds
( p in b1 iff for V being a_neighborhood of p holds N is_eventually_in V )
proof
consider IT being Subset of T such that
A1: for p being Point of T holds
( p in IT iff S1[p] ) from SUBSET_1:sch_3();
take  IT ; ::_thesis: for p being Point of T holds
( p in IT iff for V being a_neighborhood of p holds N is_eventually_in V )
let p be Point of T; ::_thesis: ( p in IT iff for V being a_neighborhood of p holds N is_eventually_in V )
thus  ( p in IT iff for V being a_neighborhood of p holds N is_eventually_in V ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of T st ( for p being Point of T holds
( p in b1 iff for V being a_neighborhood of p holds N is_eventually_in V ) ) & ( for p being Point of T holds
( p in b2 iff for V being a_neighborhood of p holds N is_eventually_in V ) ) holds
b1 = b2
proof
let it1, it2 be Subset of T; ::_thesis: ( ( for p being Point of T holds
( p in it1 iff for V being a_neighborhood of p holds N is_eventually_in V ) ) & ( for p being Point of T holds
( p in it2 iff for V being a_neighborhood of p holds N is_eventually_in V ) ) implies it1 = it2 )
assume that
A2: for p being Point of T holds
( p in it1 iff S1[p] ) and
A3: for p being Point of T holds
( p in it2 iff S1[p] ) ; ::_thesis: it1 = it2
thus  it1 = it2 from SUBSET_1:sch_4(A2, A3); ::_thesis: verum
end;
end;

:: deftheorem Def15 defines Lim YELLOW_6:def_15_:_
 for T being non empty TopSpace
for N being net of T
for b3 being Subset of T holds
( b3 = Lim N iff for p being Point of T holds
( p in b3 iff for V being a_neighborhood of p holds N is_eventually_in V ) );

theorem Th32: :: YELLOW_6:32
for T being non empty TopSpace
for N being net of T
for Y being subnet of N holds Lim N c= Lim Y
proof
let T be non empty TopSpace; ::_thesis: for N being net of T
for Y being subnet of N holds Lim N c= Lim Y
let N be net of T; ::_thesis: for Y being subnet of N holds Lim N c= Lim Y
let Y be subnet of N; ::_thesis: Lim N c= Lim Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim N or x in Lim Y )
consider f being Function of Y,N such that
A1: the mapping of Y = the mapping of N * f and
A2: for m being Element of N ex n being Element of Y st
for p being Element of Y st n <= p holds
m <= f . p by Def9;
assume A3: x in Lim N ; ::_thesis: x in Lim Y
then reconsider p = x as Point of T ;
 for V being a_neighborhood of p holds Y is_eventually_in V
proof
let V be a_neighborhood of p; ::_thesis: Y is_eventually_in V
 N is_eventually_in V by A3, Def15;
then consider ii being Element of N such that
A4: for j being Element of N st ii <= j holds
N . j in V by WAYBEL_0:def_11;
consider n being Element of Y such that
A5: for p being Element of Y st n <= p holds
ii <= f . p by A2;
take  n ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of Y holds
( not n <= b1 or Y . b1 in V )
let j be Element of Y; ::_thesis: ( not n <= j or Y . j in V )
assume A6: n <= j ; ::_thesis: Y . j in V
 N . (f . j) = Y . j by A1, FUNCT_2:15;
hence  Y . j in V by A4, A5, A6; ::_thesis: verum
end;
hence  x in Lim Y by Def15; ::_thesis: verum
end;

theorem Th33: :: YELLOW_6:33
for T being non empty TopSpace
for N being constant net of T holds the_value_of N in Lim N
proof
let T be non empty TopSpace; ::_thesis: for N being constant net of T holds the_value_of N in Lim N
let N be constant net of T; ::_thesis: the_value_of N in Lim N
set p = the_value_of N;
 for S being a_neighborhood of the_value_of N holds N is_eventually_in S
proof
set i = the Element of N;
let S be a_neighborhood of the_value_of N; ::_thesis: N is_eventually_in S
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 S )
let j be Element of N; ::_thesis: ( not the Element of N <= j or N . j in S )
assume  the Element of N <= j ; ::_thesis: N . j in S
 N . j = the_value_of N by Th16;
hence  N . j in S by CONNSP_2:4; ::_thesis: verum
end;
hence  the_value_of N in Lim N by Def15; ::_thesis: verum
end;

theorem Th34: :: YELLOW_6:34
for T being non empty TopSpace
for N being net of T
for p being Point of T st p in Lim N holds
for d being Element of N ex S being Subset of T st
( S =  {  (N . c) where c is Element of N : d <= c  }  & p in Cl S )
proof
let T be non empty TopSpace; ::_thesis: for N being net of T
for p being Point of T st p in Lim N holds
for d being Element of N ex S being Subset of T st
( S =  {  (N . c) where c is Element of N : d <= c  }  & p in Cl S )
let N be net of T; ::_thesis: for p being Point of T st p in Lim N holds
for d being Element of N ex S being Subset of T st
( S =  {  (N . c) where c is Element of N : d <= c  }  & p in Cl S )
let p be Point of T; ::_thesis: ( p in Lim N implies for d being Element of N ex S being Subset of T st
( S =  {  (N . c) where c is Element of N : d <= c  }  & p in Cl S ) )
assume A1: p in Lim N ; ::_thesis: for d being Element of N ex S being Subset of T st
( S =  {  (N . c) where c is Element of N : d <= c  }  & p in Cl S )
let d be Element of N; ::_thesis: ex S being Subset of T st
( S =  {  (N . c) where c is Element of N : d <= c  }  & p in Cl S )
  {  (N . c) where c is Element of N : d <= c  }  c= the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (N . c) where c is Element of N : d <= c  }  or x in the carrier of T )
assume  x in  {  (N . c) where c is Element of N : d <= c  }  ; ::_thesis: x in the carrier of T
then  ex c being Element of N st
( x = N . c & d <= c ) ;
hence  x in the carrier of T ; ::_thesis: verum
end;
then reconsider S =  {  (N . c) where c is Element of N : d <= c  }  as Subset of T ;
take  S ; ::_thesis: ( S =  {  (N . c) where c is Element of N : d <= c  }  & p in Cl S )
thus  S =  {  (N . c) where c is Element of N : d <= c  }  ; ::_thesis: p in Cl S
now__::_thesis:_for_G_being_a_neighborhood_of_p_holds_G_meets_S
let G be a_neighborhood of p; ::_thesis: G meets S
 N is_eventually_in G by A1, Def15;
then consider i being Element of N such that
A2: for j being Element of N st i <= j holds
N . j in G by WAYBEL_0:def_11;
consider e being Element of N such that
A3: d <= e and
A4: i <= e by Def3;
A5: N . e in S by A3;
 N . e in G by A2, A4;
hence  G meets S by A5, XBOOLE_0:3; ::_thesis: verum
end;
hence  p in Cl S by CONNSP_2:27; ::_thesis: verum
end;

theorem Th35: :: YELLOW_6:35
for T being non empty TopSpace holds
( T is Hausdorff iff for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q )
proof
let T be non empty TopSpace; ::_thesis: ( T is Hausdorff iff for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q )
thus  ( T is Hausdorff implies for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q ) ::_thesis: ( ( for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q ) implies T is Hausdorff )
proof
assume A1: T is Hausdorff ; ::_thesis: for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q
let N be net of T; ::_thesis: for p, q being Point of T st p in Lim N & q in Lim N holds
p = q
given p1, p2 being Point of T such that A2: p1 in Lim N and
A3: p2 in Lim N and
A4: p1 <> p2 ; ::_thesis: contradiction
consider W, V being Subset of T such that
A5: W is open and
A6: V is open and
A7: p1 in W and
A8: p2 in V and
A9: W misses V by A1, A4, PRE_TOPC:def_10;
 V is a_neighborhood of p2 by A6, A8, CONNSP_2:3;
then A10: N is_eventually_in V by A3, Def15;
 W is a_neighborhood of p1 by A5, A7, CONNSP_2:3;
then  N is_eventually_in W by A2, Def15;
hence  contradiction by A9, A10, Th17; ::_thesis: verum
end;
assume A11: for N being net of T
for p, q being Point of T st p in Lim N & q in Lim N holds
p = q ; ::_thesis: T is Hausdorff
given p, q being Point of T such that A12: p <> q and
A13: for W, V being Subset of T st W is open & V is open & p in W & q in V holds
W meets V ; :: according to PRE_TOPC:def_10 ::_thesis: contradiction
set pN = [:(OpenNeighborhoods p),(OpenNeighborhoods q):];
set cT = the carrier of T;
set cpN = the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):];
deffunc H1( Element of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):]) ->  set = ($1 `1) /\ ($1 `2);
A14: for i being Element of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] holds the carrier of T meets H1(i)
proof
let i be Element of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):]; ::_thesis: the carrier of T meets H1(i)
consider W being Subset of T such that
A15: W = i `1 and
A16: ( p in W & W is open ) by Th29;
consider V being Subset of T such that
A17: V = i `2 and
A18: ( q in V & V is open ) by Th29;
 i `1 meets i `2 by A13, A15, A16, A17, A18;
then  ( W /\ V c= the carrier of T & (i `1) /\ (i `2) <> {} ) by XBOOLE_0:def_7;
then  the carrier of T /\ ((i `1) /\ (i `2)) <> {} by A15, A17, XBOOLE_1:28;
hence  the carrier of T meets H1(i) by XBOOLE_0:def_7; ::_thesis: verum
end;
consider f being Function of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):], the carrier of T such that
A19: for i being Element of the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] holds f . i in H1(i) from FUNCT_2:sch_10(A14);
reconsider N = NetStr(# the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):], the InternalRel of [:(OpenNeighborhoods p),(OpenNeighborhoods q):],f #) as net of T by Lm1, Lm2;
A20: the carrier of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] = [: the carrier of (OpenNeighborhoods p), the carrier of (OpenNeighborhoods q):] by YELLOW_3:def_2;
now__::_thesis:_for_V_being_a_neighborhood_of_q_holds_N_is_eventually_in_V
let V be a_neighborhood of q; ::_thesis: N is_eventually_in V
A21: N is_eventually_in Int V
proof
A22: [#] T in the carrier of (OpenNeighborhoods p) by Th30;
 ( q in Int V & Int V is open ) by CONNSP_2:def_1;
then  Int V in the carrier of (OpenNeighborhoods q) by Th30;
then reconsider i = [([#] T),(Int V)] as Element of N by A20, A22, ZFMISC_1:87;
take  i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not i <= b1 or N . b1 in Int V )
let j be Element of N; ::_thesis: ( not i <= j or N . j in Int V )
reconsider j9 = j, i9 = i as Element of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] ;
consider j1 being Element of (OpenNeighborhoods p), j2 being Element of (OpenNeighborhoods q) such that
A23: j = [j1,j2] by A20, DOMAIN_1:1;
A24: j `2 = j2 by A23, MCART_1:7;
consider W1 being Subset of T such that
A25: j1 = W1 and
 p in W1 and
 W1 is open by Th29;
consider W2 being Subset of T such that
A26: j2 = W2 and
 q in W2 and
 W2 is open by Th29;
assume  i <= j ; ::_thesis: N . j in Int V
then  [i,j] in the InternalRel of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] by ORDERS_2:def_5;
then  i9 <= j9 by ORDERS_2:def_5;
then  ( i9 `2 = Int V & i9 `2 <= j9 `2 ) by MCART_1:7, YELLOW_3:12;
then  W2 c= Int V by A24, A26, Th31;
then A27: W1 /\ W2 c= (Int V) /\ ([#] T) by XBOOLE_1:27;
 j `1 = j1 by A23, MCART_1:7;
then  f . j in W1 /\ W2 by A19, A24, A25, A26;
then  f . j in (Int V) /\ ([#] T) by A27;
hence  N . j in Int V by XBOOLE_1:28; ::_thesis: verum
end;
 Int V c= V by TOPS_1:16;
hence  N is_eventually_in V by A21, WAYBEL_0:8; ::_thesis: verum
end;
then A28: q in Lim N by Def15;
now__::_thesis:_for_V_being_a_neighborhood_of_p_holds_N_is_eventually_in_V
let V be a_neighborhood of p; ::_thesis: N is_eventually_in V
A29: N is_eventually_in Int V
proof
A30: [#] T in the carrier of (OpenNeighborhoods q) by Th30;
 ( p in Int V & Int V is open ) by CONNSP_2:def_1;
then  Int V in the carrier of (OpenNeighborhoods p) by Th30;
then reconsider i = [(Int V),([#] T)] as Element of N by A20, A30, ZFMISC_1:87;
take  i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not i <= b1 or N . b1 in Int V )
let j be Element of N; ::_thesis: ( not i <= j or N . j in Int V )
reconsider j9 = j, i9 = i as Element of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] ;
consider j1 being Element of (OpenNeighborhoods p), j2 being Element of (OpenNeighborhoods q) such that
A31: j = [j1,j2] by A20, DOMAIN_1:1;
A32: j `1 = j1 by A31, MCART_1:7;
consider W2 being Subset of T such that
A33: j2 = W2 and
 q in W2 and
 W2 is open by Th29;
consider W1 being Subset of T such that
A34: j1 = W1 and
 p in W1 and
 W1 is open by Th29;
assume  i <= j ; ::_thesis: N . j in Int V
then  [i,j] in the InternalRel of [:(OpenNeighborhoods p),(OpenNeighborhoods q):] by ORDERS_2:def_5;
then  i9 <= j9 by ORDERS_2:def_5;
then  ( i9 `1 = Int V & i9 `1 <= j9 `1 ) by MCART_1:7, YELLOW_3:12;
then  W1 c= Int V by A32, A34, Th31;
then A35: W1 /\ W2 c= (Int V) /\ ([#] T) by XBOOLE_1:27;
 j `2 = j2 by A31, MCART_1:7;
then  f . j in W1 /\ W2 by A19, A32, A34, A33;
then  f . j in (Int V) /\ ([#] T) by A35;
hence  N . j in Int V by XBOOLE_1:28; ::_thesis: verum
end;
 Int V c= V by TOPS_1:16;
hence  N is_eventually_in V by A29, WAYBEL_0:8; ::_thesis: verum
end;
then  p in Lim N by Def15;
hence  contradiction by A11, A12, A28; ::_thesis: verum
end;

registration
let T be non empty Hausdorff TopSpace;
let N be net of T;
cluster Lim N ->  trivial ;
coherence
 Lim N is trivial
proof
 for p, q being Point of T st p in Lim N & q in Lim N holds
p = q by Th35;
hence  Lim N is trivial by SUBSET_1:45; ::_thesis: verum
end;
end;

definition
let T be non empty TopSpace;
let N be net of T;
attrN is convergent  means :Def16: :: YELLOW_6:def 16
 Lim N <> {} ;
end;

:: deftheorem Def16 defines convergent YELLOW_6:def_16_:_
 for T being non empty TopSpace
for N being net of T holds
( N is convergent iff Lim N <> {} );

registration
let T be non empty TopSpace;
cluster non empty transitive directed constant  ->  convergent for NetStr over T;
coherence
 for b1 being net of T st b1 is constant holds
b1 is convergent
proof
let N be net of T; ::_thesis: ( N is constant implies N is convergent )
assume  N is constant ; ::_thesis: N is convergent
hence  Lim N <> {} by Th33; :: according to YELLOW_6:def_16 ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
cluster non empty transitive strict directed convergent for NetStr over T;
existence
 ex b1 being net of T st
( b1 is convergent & b1 is strict )
proof
set R = the non empty transitive directed RelStr ;
set p = the Point of T;
take  ConstantNet ( the non empty transitive directed RelStr , the Point of T) ; ::_thesis: ( ConstantNet ( the non empty transitive directed RelStr , the Point of T) is convergent & ConstantNet ( the non empty transitive directed RelStr , the Point of T) is strict )
thus  ( ConstantNet ( the non empty transitive directed RelStr , the Point of T) is convergent & ConstantNet ( the non empty transitive directed RelStr , the Point of T) is strict ) ; ::_thesis: verum
end;
end;

definition
let T be non empty Hausdorff TopSpace;
let N be convergent net of T;
func lim N ->  Element of T means :Def17: :: YELLOW_6:def 17
it in Lim N;
existence
 ex b1 being Element of T st b1 in Lim N
proof
 Lim N <> {} by Def16;
then consider p being Point of T such that
A1: p in Lim N by SUBSET_1:4;
take  p ; ::_thesis: p in Lim N
thus  p in Lim N by A1; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of T st b1 in Lim N & b2 in Lim N holds
b1 = b2;
by ZFMISC_1:def_10;
end;

:: deftheorem Def17 defines lim YELLOW_6:def_17_:_
 for T being non empty Hausdorff TopSpace
for N being convergent net of T
for b3 being Element of T holds
( b3 = lim N iff b3 in Lim N );

theorem :: YELLOW_6:36
for T being non empty Hausdorff TopSpace
for N being constant net of T holds lim N = the_value_of N
proof
let T be non empty Hausdorff TopSpace; ::_thesis: for N being constant net of T holds lim N = the_value_of N
let N be constant net of T; ::_thesis: lim N = the_value_of N
 the_value_of N in Lim N by Th33;
hence  lim N = the_value_of N by Def17; ::_thesis: verum
end;

theorem :: YELLOW_6:37
for T being non empty TopSpace
for N being net of T
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z
proof
let T be non empty TopSpace; ::_thesis: for N being net of T
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z
let N be net of T; ::_thesis: for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z
let p be Point of T; ::_thesis: ( not p in Lim N implies ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z )
assume  not p in Lim N ; ::_thesis: ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z
then consider V being a_neighborhood of p such that
A1: not N is_eventually_in V by Def15;
 N is_often_in the carrier of T \ V by A1, WAYBEL_0:9;
then reconsider Y = N " ( the carrier of T \ V) as subnet of N by Th22;
take  Y ; ::_thesis: for Z being subnet of Y holds not p in Lim Z
let Z be subnet of Y; ::_thesis: not p in Lim Z
assume  p in Lim Z ; ::_thesis: contradiction
then  Z is_eventually_in V by Def15;
then A2: Y is_often_in V by Th18, Th19;
 Y is_eventually_in the carrier of T \ V by Th23;
hence  contradiction by A2, WAYBEL_0:10; ::_thesis: verum
end;

theorem Th38: :: YELLOW_6:38
for T being non empty TopSpace
for N being net of T st N in NetUniv T holds
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
proof
let T be non empty TopSpace; ::_thesis: for N being net of T st N in NetUniv T holds
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
let N be net of T; ::_thesis: ( N in NetUniv T implies for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) ) )
assume  N in NetUniv T ; ::_thesis: for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
then A1: ex M being strict net of T st
( M = N & the carrier of M in the_universe_of the carrier of T ) by Def11;
let p be Point of T; ::_thesis: ( not p in Lim N implies ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) ) )
assume  not p in Lim N ; ::_thesis: ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
then consider V being a_neighborhood of p such that
A2: not N is_eventually_in V by Def15;
 N is_often_in the carrier of T \ V by A2, WAYBEL_0:9;
then reconsider Y = N " ( the carrier of T \ V) as subnet of N by Th22;
take  Y ; ::_thesis: ( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
 the carrier of Y = the mapping of N " ( the carrier of T \ V) by Def10;
then  the carrier of Y in the_universe_of the carrier of T by A1, CLASSES1:def_1;
hence  Y in NetUniv T by Def11; ::_thesis: for Z being subnet of Y holds not p in Lim Z
let Z be subnet of Y; ::_thesis: not p in Lim Z
assume  p in Lim Z ; ::_thesis: contradiction
then  Z is_eventually_in V by Def15;
then A3: Y is_often_in V by Th18, Th19;
 Y is_eventually_in the carrier of T \ V by Th23;
hence  contradiction by A3, WAYBEL_0:10; ::_thesis: verum
end;

theorem Th39: :: YELLOW_6:39
for T being non empty TopSpace
for N being net of T
for p being Point of T st p in Lim N holds
for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
proof
let T be non empty TopSpace; ::_thesis: for N being net of T
for p being Point of T st p in Lim N holds
for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let N be net of T; ::_thesis: for p being Point of T st p in Lim N holds
for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let p be Point of T; ::_thesis: ( p in Lim N implies for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J) )
assume A1: p in Lim N ; ::_thesis: for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let J be net_set of the carrier of N,T; ::_thesis: ( ( for i being Element of N holds N . i in Lim (J . i) ) implies p in Lim (Iterated J) )
assume A2: for i being Element of N holds N . i in Lim (J . i) ; ::_thesis: p in Lim (Iterated J)
 for V being a_neighborhood of p holds Iterated J is_eventually_in V
proof
let V be a_neighborhood of p; ::_thesis: Iterated J is_eventually_in V
 p in Int (Int V) by CONNSP_2:def_1;
then reconsider W = Int V as a_neighborhood of p by CONNSP_2:def_1;
 N is_eventually_in W by A1, Def15;
then consider i being Element of N such that
A3: for j being Element of N st i <= j holds
N . j in W by WAYBEL_0:def_11;
defpred S1[ Element of N, set ] means  ex m being Element of (J . $1) st
( m = $2 & ( i <= $1 implies for n being Element of (J . $1) st m <= n holds
(J . $1) . n in W ) );
A4: Int V = Int (Int V) ;
A5: for j being Element of N ex e being set st S1[j,e]
proof
let j be Element of N; ::_thesis: ex e being set st S1[j,e]
reconsider j9 = j as Element of N ;
percases ( i <= j or not i <= j ) ;
suppose i <= j ; ::_thesis: ex e being set st S1[j,e]
then  N . j9 in W by A3;
then A6: W is a_neighborhood of N . j by A4, CONNSP_2:def_1;
 N . j in Lim (J . j) by A2;
then  J . j is_eventually_in W by A6, Def15;
then consider e being Element of (J . j) such that
A7: for u being Element of (J . j) st e <= u holds
(J . j) . u in W by WAYBEL_0:def_11;
take  e ; ::_thesis: S1[j,e]
take  e ; ::_thesis: ( e = e & ( i <= j implies for n being Element of (J . j) st e <= n holds
(J . j) . n in W ) )
thus  e = e ; ::_thesis: ( i <= j implies for n being Element of (J . j) st e <= n holds
(J . j) . n in W )
assume  i <= j ; ::_thesis: for n being Element of (J . j) st e <= n holds
(J . j) . n in W
thus  for n being Element of (J . j) st e <= n holds
(J . j) . n in W by A7; ::_thesis: verum
end;
supposeA8: not i <= j ; ::_thesis: ex e being set st S1[j,e]
set e = the Element of (J . j);
take  the Element of (J . j) ; ::_thesis: S1[j, the Element of (J . j)]
take  the Element of (J . j) ; ::_thesis: ( the Element of (J . j) = the Element of (J . j) & ( i <= j implies for n being Element of (J . j) st the Element of (J . j) <= n holds
(J . j) . n in W ) )
thus  ( the Element of (J . j) = the Element of (J . j) & ( i <= j implies for n being Element of (J . j) st the Element of (J . j) <= n holds
(J . j) . n in W ) ) by A8; ::_thesis: verum
end;
end;
end;
consider f being ManySortedSet of the carrier of N such that
A9: for j being Element of N holds S1[j,f . j] from PBOOLE:sch_6(A5);
A10: for x being set st x in dom (Carrier J) holds
f . x in (Carrier J) . x
proof
let x be set ; ::_thesis: ( x in dom (Carrier J) implies f . x in (Carrier J) . x )
assume  x in dom (Carrier J) ; ::_thesis: f . x in (Carrier J) . x
then reconsider j = x as Element of N ;
 ex m being Element of (J . j) st
( m = f . j & ( i <= j implies for n being Element of (J . j) st m <= n holds
(J . j) . n in W ) ) by A9;
then  f . x in the carrier of (J . j) ;
hence  f . x in (Carrier J) . x by Th2; ::_thesis: verum
end;
 dom (Carrier J) = the carrier of N by PARTFUN1:def_2;
then  dom f = dom (Carrier J) by PARTFUN1:def_2;
then A11: f in product (Carrier J) by A10, CARD_3:9;
A12: the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):] by Th26;
then reconsider x = [i,f] as Element of (Iterated J) by A11, ZFMISC_1:87;
take  x ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (Iterated J) holds
( not x <= b1 or (Iterated J) . b1 in V )
let j be Element of (Iterated J); ::_thesis: ( not x <= j or (Iterated J) . j in V )
assume A13: x <= j ; ::_thesis: (Iterated J) . j in V
consider j1 being Element of N, j2 being Element of product (Carrier J) such that
A14: j = [j1,j2] by A12, DOMAIN_1:1;
reconsider j2 = j2, i2 = f as Element of (product J) by A11, YELLOW_1:def_4;
reconsider i1 = i, j1 = j1 as Element of N ;
 i2 in the carrier of (product J) ;
then A15: i2 in product (Carrier J) by YELLOW_1:def_4;
 RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = [:N,(product J):] by Def13;
then A16: [i1,i2] <= [j1,j2] by A13, A14, YELLOW_0:1;
then  i2 <= j2 by YELLOW_3:11;
then  ex f, g being Function st
( f = i2 & g = j2 & ( for i being set st i in the carrier of N holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A15, YELLOW_1:def_4;
then A17: ex R being RelStr ex xi, yi being Element of R st
( R = J . j1 & xi = i2 . j1 & yi = j2 . j1 & xi <= yi ) ;
 ex m being Element of (J . j1) st
( m = f . j1 & ( i <= j1 implies for n being Element of (J . j1) st m <= n holds
(J . j1) . n in W ) ) by A9;
then  (J . j1) . (j2 . j1) in W by A16, A17, YELLOW_3:11;
then A18: (Iterated J) . j in W by A14, Th27;
 W c= V by TOPS_1:16;
hence  (Iterated J) . j in V by A18; ::_thesis: verum
end;
hence  p in Lim (Iterated J) by Def15; ::_thesis: verum
end;

begin

definition
let S be non empty 1-sorted ;
mode Convergence-Class of S ->  set  means :Def18: :: YELLOW_6:def 18
it c= [:(NetUniv S), the carrier of S:];
existence
 ex b1 being set st b1 c= [:(NetUniv S), the carrier of S:] ;
end;

:: deftheorem Def18 defines Convergence-Class YELLOW_6:def_18_:_
 for S being non empty 1-sorted
for b2 being set holds
( b2 is Convergence-Class of S iff b2 c= [:(NetUniv S), the carrier of S:] );

registration
let S be non empty 1-sorted ;
cluster  ->  Relation-like for Convergence-Class of S;
coherence
 for b1 being Convergence-Class of S holds b1 is Relation-like
proof
let C be Convergence-Class of S; ::_thesis: C is Relation-like
 C is Subset of [:(NetUniv S), the carrier of S:] by Def18;
hence  C is Relation-like ; ::_thesis: verum
end;
end;

definition
let T be non empty TopSpace;
func Convergence T ->  Convergence-Class of T means :Def19: :: YELLOW_6:def 19
 for N being net of T
for p being Point of T holds
( [N,p] in it iff ( N in NetUniv T & p in Lim N ) );
existence
 ex b1 being Convergence-Class of T st
for N being net of T
for p being Point of T holds
( [N,p] in b1 iff ( N in NetUniv T & p in Lim N ) )
proof
defpred S1[ set , set ] means  ex N being net of T ex p being Point of T st
( N = $1 & p = $2 & p in Lim N );
consider R being Relation of (NetUniv T), the carrier of T such that
A1: for x, y being set holds
( [x,y] in R iff ( x in NetUniv T & y in the carrier of T & S1[x,y] ) ) from RELSET_1:sch_1();
reconsider R = R as Convergence-Class of T by Def18;
take  R ; ::_thesis: for N being net of T
for p being Point of T holds
( [N,p] in R iff ( N in NetUniv T & p in Lim N ) )
let N be net of T; ::_thesis: for p being Point of T holds
( [N,p] in R iff ( N in NetUniv T & p in Lim N ) )
let p be Point of T; ::_thesis: ( [N,p] in R iff ( N in NetUniv T & p in Lim N ) )
hereby  ::_thesis: ( N in NetUniv T & p in Lim N implies [N,p] in R )
assume A2: [N,p] in R ; ::_thesis: ( N in NetUniv T & p in Lim N )
hence  N in NetUniv T by A1; ::_thesis: p in Lim N
 ex N9 being net of T ex p9 being Point of T st
( N9 = N & p9 = p & p9 in Lim N9 ) by A1, A2;
hence  p in Lim N ; ::_thesis: verum
end;
thus  ( N in NetUniv T & p in Lim N implies [N,p] in R ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Convergence-Class of T st ( for N being net of T
for p being Point of T holds
( [N,p] in b1 iff ( N in NetUniv T & p in Lim N ) ) ) & ( for N being net of T
for p being Point of T holds
( [N,p] in b2 iff ( N in NetUniv T & p in Lim N ) ) ) holds
b1 = b2
proof
let it1, it2 be Convergence-Class of T; ::_thesis: ( ( for N being net of T
for p being Point of T holds
( [N,p] in it1 iff ( N in NetUniv T & p in Lim N ) ) ) & ( for N being net of T
for p being Point of T holds
( [N,p] in it2 iff ( N in NetUniv T & p in Lim N ) ) ) implies it1 = it2 )
assume that
A3: for N being net of T
for p being Point of T holds
( [N,p] in it1 iff ( N in NetUniv T & p in Lim N ) ) and
A4: for N being net of T
for p being Point of T holds
( [N,p] in it2 iff ( N in NetUniv T & p in Lim N ) ) ; ::_thesis: it1 = it2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in it1 or [x,b1] in it2 ) & ( not [x,b1] in it2 or [x,b1] in it1 ) )
let y be set ; ::_thesis: ( ( not [x,y] in it1 or [x,y] in it2 ) & ( not [x,y] in it2 or [x,y] in it1 ) )
A5: it1 c= [:(NetUniv T), the carrier of T:] by Def18;
thus  ( [x,y] in it1 implies [x,y] in it2 ) ::_thesis: ( not [x,y] in it2 or [x,y] in it1 )
proof
assume A6: [x,y] in it1 ; ::_thesis: [x,y] in it2
then reconsider p = y as Point of T by A5, ZFMISC_1:87;
 x in NetUniv T by A5, A6, ZFMISC_1:87;
then consider N being strict net of T such that
A7: N = x and
 the carrier of N in the_universe_of the carrier of T by Def11;
 [N,p] in it1 by A6, A7;
then A8: N in NetUniv T by A3;
 p in Lim N by A3, A6, A7;
hence  [x,y] in it2 by A4, A7, A8; ::_thesis: verum
end;
assume A9: [x,y] in it2 ; ::_thesis: [x,y] in it1
A10: it2 c= [:(NetUniv T), the carrier of T:] by Def18;
then reconsider p = y as Point of T by A9, ZFMISC_1:87;
 x in NetUniv T by A10, A9, ZFMISC_1:87;
then consider N being strict net of T such that
A11: N = x and
 the carrier of N in the_universe_of the carrier of T by Def11;
 [N,p] in it2 by A9, A11;
then A12: N in NetUniv T by A4;
 p in Lim N by A4, A9, A11;
hence  [x,y] in it1 by A3, A11, A12; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines Convergence YELLOW_6:def_19_:_
 for T being non empty TopSpace
for b2 being Convergence-Class of T holds
( b2 = Convergence T iff for N being net of T
for p being Point of T holds
( [N,p] in b2 iff ( N in NetUniv T & p in Lim N ) ) );

definition
let T be non empty 1-sorted ;
let C be Convergence-Class of T;
attrC is (CONSTANTS)  means :Def20: :: YELLOW_6:def 20
 for N being constant net of T st N in NetUniv T holds
[N,(the_value_of N)] in C;
attrC is (SUBNETS)  means :Def21: :: YELLOW_6:def 21
 for N being net of T
for Y being subnet of N st Y in NetUniv T holds
for p being Element of T st [N,p] in C holds
[Y,p] in C;
attrC is (DIVERGENCE)  means :Def22: :: YELLOW_6:def 22
 for X being net of T
for p being Element of T st X in NetUniv T & not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) );
attrC is (ITERATED_LIMITS)  means :Def23: :: YELLOW_6:def 23
 for X being net of T
for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C;
end;

:: deftheorem Def20 defines (CONSTANTS) YELLOW_6:def_20_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (CONSTANTS) iff for N being constant net of T st N in NetUniv T holds
[N,(the_value_of N)] in C );

:: deftheorem Def21 defines (SUBNETS) YELLOW_6:def_21_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (SUBNETS) iff for N being net of T
for Y being subnet of N st Y in NetUniv T holds
for p being Element of T st [N,p] in C holds
[Y,p] in C );

:: deftheorem Def22 defines (DIVERGENCE) YELLOW_6:def_22_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (DIVERGENCE) iff for X being net of T
for p being Element of T st X in NetUniv T & not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) );

:: deftheorem Def23 defines (ITERATED_LIMITS) YELLOW_6:def_23_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (ITERATED_LIMITS) iff for X being net of T
for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C );

registration
let T be non empty TopSpace;
cluster Convergence T ->  (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) ;
coherence
 ( Convergence T is (CONSTANTS) & Convergence T is (SUBNETS) & Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )
proof
set C = Convergence T;
thus  Convergence T is (CONSTANTS) ::_thesis: ( Convergence T is (SUBNETS) & Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )
proof
let N be constant net of T; :: according to YELLOW_6:def_20 ::_thesis: ( N in NetUniv T implies [N,(the_value_of N)] in Convergence T )
assume A1: N in NetUniv T ; ::_thesis: [N,(the_value_of N)] in Convergence T
 the_value_of N in Lim N by Th33;
hence  [N,(the_value_of N)] in Convergence T by A1, Def19; ::_thesis: verum
end;
thus  Convergence T is (SUBNETS) ::_thesis: ( Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )
proof
let N be net of T; :: according to YELLOW_6:def_21 ::_thesis: for Y being subnet of N st Y in NetUniv T holds
for p being Element of T st [N,p] in Convergence T holds
[Y,p] in Convergence T
let Y be subnet of N; ::_thesis: ( Y in NetUniv T implies for p being Element of T st [N,p] in Convergence T holds
[Y,p] in Convergence T )
assume A2: Y in NetUniv T ; ::_thesis: for p being Element of T st [N,p] in Convergence T holds
[Y,p] in Convergence T
let p be Element of T; ::_thesis: ( [N,p] in Convergence T implies [Y,p] in Convergence T )
assume  [N,p] in Convergence T ; ::_thesis: [Y,p] in Convergence T
then A3: p in Lim N by Def19;
 Lim N c= Lim Y by Th32;
hence  [Y,p] in Convergence T by A2, A3, Def19; ::_thesis: verum
end;
thus  Convergence T is (DIVERGENCE) ::_thesis: Convergence T is (ITERATED_LIMITS)
proof
let X be net of T; :: according to YELLOW_6:def_22 ::_thesis: for p being Element of T st X in NetUniv T & not [X,p] in Convergence T holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) )
let p be Element of T; ::_thesis: ( X in NetUniv T & not [X,p] in Convergence T implies ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) ) )
assume A4: X in NetUniv T ; ::_thesis: ( [X,p] in Convergence T or ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) ) )
assume  not [X,p] in Convergence T ; ::_thesis: ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) )
then  not p in Lim X by A4, Def19;
then consider Y being subnet of X such that
A5: Y in NetUniv T and
A6: for Z being subnet of Y holds not p in Lim Z by A4, Th38;
take  Y ; ::_thesis: ( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) )
thus  Y in NetUniv T by A5; ::_thesis: for Z being subnet of Y holds not [Z,p] in Convergence T
let Z be subnet of Y; ::_thesis: not [Z,p] in Convergence T
 not p in Lim Z by A6;
hence  not [Z,p] in Convergence T by Def19; ::_thesis: verum
end;
let X be net of T; :: according to YELLOW_6:def_23 ::_thesis: for p being Element of T st [X,p] in Convergence T holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in Convergence T ) holds
[(Iterated J),p] in Convergence T
let p be Element of T; ::_thesis: ( [X,p] in Convergence T implies for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in Convergence T ) holds
[(Iterated J),p] in Convergence T )
assume A7: [X,p] in Convergence T ; ::_thesis: for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in Convergence T ) holds
[(Iterated J),p] in Convergence T
let J be net_set of the carrier of X,T; ::_thesis: ( ( for i being Element of X holds [(J . i),(X . i)] in Convergence T ) implies [(Iterated J),p] in Convergence T )
assume A8: for i being Element of X holds [(J . i),(X . i)] in Convergence T ; ::_thesis: [(Iterated J),p] in Convergence T
A9: now__::_thesis:_for_i_being_Element_of_X_holds_
(_X_._i_in_Lim_(J_._i)_&_J_._i_in_NetUniv_T_)
let i be Element of X; ::_thesis: ( X . i in Lim (J . i) & J . i in NetUniv T )
 [(J . i),(X . i)] in Convergence T by A8;
hence  ( X . i in Lim (J . i) & J . i in NetUniv T ) by Def19; ::_thesis: verum
end;
 X in NetUniv T by A7, Def19;
then A10: Iterated J in NetUniv T by A9, Th25;
 p in Lim X by A7, Def19;
then  p in Lim (Iterated J) by A9, Th39;
hence  [(Iterated J),p] in Convergence T by A10, Def19; ::_thesis: verum
end;
end;

definition
let S be non empty 1-sorted ;
let C be Convergence-Class of S;
func ConvergenceSpace C ->  strict TopStruct  means :Def24: :: YELLOW_6:def 24
( the carrier of it = the carrier of S & the topology of it =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  );
existence
 ex b1 being strict TopStruct st
( the carrier of b1 = the carrier of S & the topology of b1 =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  )
proof
defpred S1[ set ] means  for p being Element of S st p in $1 holds
for N being net of S st [N,p] in C holds
N is_eventually_in $1;
reconsider X =  {  V where V is Subset of S : S1[V]  }  as Subset-Family of S from DOMAIN_1:sch_7();
take  TopStruct(# the carrier of S,X #) ; ::_thesis: ( the carrier of TopStruct(# the carrier of S,X #) = the carrier of S & the topology of TopStruct(# the carrier of S,X #) =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  )
thus  ( the carrier of TopStruct(# the carrier of S,X #) = the carrier of S & the topology of TopStruct(# the carrier of S,X #) =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = the carrier of S & the topology of b1 =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  & the carrier of b2 = the carrier of S & the topology of b2 =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  holds
b1 = b2;
;
end;

:: deftheorem Def24 defines ConvergenceSpace YELLOW_6:def_24_:_
 for S being non empty 1-sorted
for C being Convergence-Class of S
for b3 being strict TopStruct holds
( b3 = ConvergenceSpace C iff ( the carrier of b3 = the carrier of S & the topology of b3 =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  ) );

registration
let S be non empty 1-sorted ;
let C be Convergence-Class of S;
cluster ConvergenceSpace C ->  non empty strict ;
coherence
 not ConvergenceSpace C is empty
proof
 the carrier of (ConvergenceSpace C) = the carrier of S by Def24;
hence  not the carrier of (ConvergenceSpace C) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
let S be non empty 1-sorted ;
let C be Convergence-Class of S;
cluster ConvergenceSpace C ->  strict TopSpace-like ;
coherence
 ConvergenceSpace C is TopSpace-like
proof
set IT = ConvergenceSpace C;
A1: the topology of (ConvergenceSpace C) =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  by Def24;
reconsider V = [#] (ConvergenceSpace C) as Subset of S by Def24;
 V = the carrier of S by Def24;
then  for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V by Th20;
hence  the carrier of (ConvergenceSpace C) in the topology of (ConvergenceSpace C) by A1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of (ConvergenceSpace C)) holds
( not b1 c= the topology of (ConvergenceSpace C) or union b1 in the topology of (ConvergenceSpace C) ) ) & ( for b1, b2 being Element of bool the carrier of (ConvergenceSpace C) holds
( not b1 in the topology of (ConvergenceSpace C) or not b2 in the topology of (ConvergenceSpace C) or b1 /\ b2 in the topology of (ConvergenceSpace C) ) ) )
hereby  ::_thesis: for b1, b2 being Element of bool the carrier of (ConvergenceSpace C) holds
( not b1 in the topology of (ConvergenceSpace C) or not b2 in the topology of (ConvergenceSpace C) or b1 /\ b2 in the topology of (ConvergenceSpace C) )
let a be Subset-Family of (ConvergenceSpace C); ::_thesis: ( a c= the topology of (ConvergenceSpace C) implies union a in the topology of (ConvergenceSpace C) )
assume A2: a c= the topology of (ConvergenceSpace C) ; ::_thesis: union a in the topology of (ConvergenceSpace C)
reconsider V = union a as Subset of S by Def24;
now__::_thesis:_for_p_being_Element_of_S_st_p_in_V_holds_
for_N_being_net_of_S_st_[N,p]_in_C_holds_
N_is_eventually_in_V
let p be Element of S; ::_thesis: ( p in V implies for N being net of S st [N,p] in C holds
N is_eventually_in V )
assume  p in V ; ::_thesis: for N being net of S st [N,p] in C holds
N is_eventually_in V
then consider X being set  such that
A3: p in X and
A4: X in a by TARSKI:def_4;
A5: X c= V by A4, ZFMISC_1:74;
 X in the topology of (ConvergenceSpace C) by A2, A4;
then A6: ex W being Subset of S st
( X = W & ( for p being Element of S st p in W holds
for N being net of S st [N,p] in C holds
N is_eventually_in W ) ) by A1;
let N be net of S; ::_thesis: ( [N,p] in C implies N is_eventually_in V )
assume  [N,p] in C ; ::_thesis: N is_eventually_in V
hence  N is_eventually_in V by A3, A6, A5, WAYBEL_0:8; ::_thesis: verum
end;
hence  union a in the topology of (ConvergenceSpace C) by A1; ::_thesis: verum
end;
let a, b be Subset of (ConvergenceSpace C); ::_thesis: ( not a in the topology of (ConvergenceSpace C) or not b in the topology of (ConvergenceSpace C) or a /\ b in the topology of (ConvergenceSpace C) )
assume  a in the topology of (ConvergenceSpace C) ; ::_thesis: ( not b in the topology of (ConvergenceSpace C) or a /\ b in the topology of (ConvergenceSpace C) )
then consider Va being Subset of S such that
A7: a = Va and
A8: for p being Element of S st p in Va holds
for N being net of S st [N,p] in C holds
N is_eventually_in Va by A1;
reconsider V = a /\ b as Subset of S by Def24;
assume  b in the topology of (ConvergenceSpace C) ; ::_thesis: a /\ b in the topology of (ConvergenceSpace C)
then consider Vb being Subset of S such that
A9: b = Vb and
A10: for p being Element of S st p in Vb holds
for N being net of S st [N,p] in C holds
N is_eventually_in Vb by A1;
now__::_thesis:_for_p_being_Element_of_S_st_p_in_V_holds_
for_N_being_net_of_S_st_[N,p]_in_C_holds_
N_is_eventually_in_V
let p be Element of S; ::_thesis: ( p in V implies for N being net of S st [N,p] in C holds
N is_eventually_in V )
assume A11: p in V ; ::_thesis: for N being net of S st [N,p] in C holds
N is_eventually_in V
let N be net of S; ::_thesis: ( [N,p] in C implies N is_eventually_in V )
assume A12: [N,p] in C ; ::_thesis: N is_eventually_in V
 p in b by A11, XBOOLE_0:def_4;
then  N is_eventually_in Vb by A9, A10, A12;
then consider i2 being Element of N such that
A13: for j being Element of N st i2 <= j holds
N . j in Vb by WAYBEL_0:def_11;
 p in a by A11, XBOOLE_0:def_4;
then  N is_eventually_in Va by A7, A8, A12;
then consider i1 being Element of N such that
A14: for j being Element of N st i1 <= j holds
N . j in Va by WAYBEL_0:def_11;
consider i being Element of N such that
A15: i1 <= i and
A16: i2 <= i by Def3;
thus  N is_eventually_in V ::_thesis: verum
proof
take  i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not i <= b1 or N . b1 in V )
let j be Element of N; ::_thesis: ( not i <= j or N . j in V )
assume A17: i <= j ; ::_thesis: N . j in V
then  i2 <= j by A16, YELLOW_0:def_2;
then A18: N . j in Vb by A13;
 i1 <= j by A15, A17, YELLOW_0:def_2;
then  N . j in Va by A14;
hence  N . j in V by A7, A9, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
hence  a /\ b in the topology of (ConvergenceSpace C) by A1; ::_thesis: verum
end;
end;

theorem Th40: :: YELLOW_6:40
for S being non empty 1-sorted
for C being Convergence-Class of S holds C c= Convergence (ConvergenceSpace C)
proof
let S be non empty 1-sorted ; ::_thesis: for C being Convergence-Class of S holds C c= Convergence (ConvergenceSpace C)
let C be Convergence-Class of S; ::_thesis: C c= Convergence (ConvergenceSpace C)
set T = ConvergenceSpace C;
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in C or [x,b1] in Convergence (ConvergenceSpace C) )
let y be set ; ::_thesis: ( not [x,y] in C or [x,y] in Convergence (ConvergenceSpace C) )
assume A1: [x,y] in C ; ::_thesis: [x,y] in Convergence (ConvergenceSpace C)
 C c= [:(NetUniv S), the carrier of S:] by Def18;
then consider M being Element of NetUniv S, p being Element of S such that
A2: [x,y] = [M,p] by A1, DOMAIN_1:1;
reconsider q = p as Point of (ConvergenceSpace C) by Def24;
A3: ( the carrier of S = the carrier of (ConvergenceSpace C) & M in NetUniv S ) by Def24;
 ex N being strict net of S st
( N = M & the carrier of N in the_universe_of the carrier of S ) by Def11;
then reconsider M = M as net of S ;
reconsider N = M as net of ConvergenceSpace C by Def24;
A4: the topology of (ConvergenceSpace C) =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  by Def24;
now__::_thesis:_for_V_being_a_neighborhood_of_q_holds_N_is_eventually_in_V
let V be a_neighborhood of q; ::_thesis: N is_eventually_in V
 Int V in the topology of (ConvergenceSpace C) by PRE_TOPC:def_2;
then  ( p in Int V & ex W being Subset of S st
( W = Int V & ( for p being Element of S st p in W holds
for N being net of S st [N,p] in C holds
N is_eventually_in W ) ) ) by A4, CONNSP_2:def_1;
then  M is_eventually_in Int V by A1, A2;
then consider ii being Element of M such that
A5: for j being Element of M st ii <= j holds
M . j in Int V by WAYBEL_0:def_11;
reconsider i = ii as Element of N ;
now__::_thesis:_for_j_being_Element_of_N_st_i_<=_j_holds_
N_._j_in_Int_V
let j be Element of N; ::_thesis: ( i <= j implies N . j in Int V )
assume A6: i <= j ; ::_thesis: N . j in Int V
reconsider jj = j as Element of M ;
 M . jj = N . j ;
hence  N . j in Int V by A5, A6; ::_thesis: verum
end;
then  ( Int V c= V & N is_eventually_in Int V ) by TOPS_1:16, WAYBEL_0:def_11;
hence  N is_eventually_in V by WAYBEL_0:8; ::_thesis: verum
end;
then A7: p in Lim N by Def15;
 N in NetUniv (ConvergenceSpace C) by A3, Lm7;
hence  [x,y] in Convergence (ConvergenceSpace C) by A2, A7, Def19; ::_thesis: verum
end;

definition
let T be non empty 1-sorted ;
let C be Convergence-Class of T;
attrC is topological  means :Def25: :: YELLOW_6:def 25
( C is (CONSTANTS) & C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) );
end;

:: deftheorem Def25 defines topological YELLOW_6:def_25_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is topological iff ( C is (CONSTANTS) & C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) ) );

registration
let T be non empty 1-sorted ;
cluster Relation-like non empty topological for Convergence-Class of T;
existence
 ex b1 being Convergence-Class of T st
( not b1 is empty & b1 is topological )
proof
reconsider C = [:(NetUniv T), the carrier of T:] as Convergence-Class of T by Def18;
take  C ; ::_thesis: ( not C is empty & C is topological )
thus  not C is empty ; ::_thesis: C is topological
thus  C is topological ::_thesis: verum
proof
thus  C is (CONSTANTS) :: according to YELLOW_6:def_25 ::_thesis: ( C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
proof
let N be constant net of T; :: according to YELLOW_6:def_20 ::_thesis: ( N in NetUniv T implies [N,(the_value_of N)] in C )
thus  ( N in NetUniv T implies [N,(the_value_of N)] in C ) by ZFMISC_1:87; ::_thesis: verum
end;
thus  C is (SUBNETS) ::_thesis: ( C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
proof
let N be net of T; :: according to YELLOW_6:def_21 ::_thesis: for Y being subnet of N st Y in NetUniv T holds
for p being Element of T st [N,p] in C holds
[Y,p] in C
let Y be subnet of N; ::_thesis: ( Y in NetUniv T implies for p being Element of T st [N,p] in C holds
[Y,p] in C )
thus  ( Y in NetUniv T implies for p being Element of T st [N,p] in C holds
[Y,p] in C ) by ZFMISC_1:87; ::_thesis: verum
end;
thus  C is (DIVERGENCE) ::_thesis: C is (ITERATED_LIMITS)
proof
let X be net of T; :: according to YELLOW_6:def_22 ::_thesis: for p being Element of T st X in NetUniv T & not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) )
let p be Element of T; ::_thesis: ( X in NetUniv T & not [X,p] in C implies ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) )
thus  ( X in NetUniv T & not [X,p] in C implies ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) ) by ZFMISC_1:87; ::_thesis: verum
end;
let X be net of T; :: according to YELLOW_6:def_23 ::_thesis: for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C
let p be Element of T; ::_thesis: ( [X,p] in C implies for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C )
assume  [X,p] in C ; ::_thesis: for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C
then A1: X in NetUniv T by ZFMISC_1:87;
let J be net_set of the carrier of X,T; ::_thesis: ( ( for i being Element of X holds [(J . i),(X . i)] in C ) implies [(Iterated J),p] in C )
assume A2: for i being Element of X holds [(J . i),(X . i)] in C ; ::_thesis: [(Iterated J),p] in C
now__::_thesis:_for_i_being_Element_of_X_holds_J_._i_in_NetUniv_T
let i be Element of X; ::_thesis: J . i in NetUniv T
 [(J . i),(X . i)] in C by A2;
hence  J . i in NetUniv T by ZFMISC_1:87; ::_thesis: verum
end;
then  Iterated J in NetUniv T by A1, Th25;
hence  [(Iterated J),p] in C by ZFMISC_1:87; ::_thesis: verum
end;
end;
end;

registration
let T be non empty 1-sorted ;
cluster topological  ->  (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) for Convergence-Class of T;
coherence
 for b1 being Convergence-Class of T st b1 is topological holds
( b1 is (CONSTANTS) & b1 is (SUBNETS) & b1 is (DIVERGENCE) & b1 is (ITERATED_LIMITS) ) by Def25;
cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS)  ->  topological for Convergence-Class of T;
coherence
 for b1 being Convergence-Class of T st b1 is (CONSTANTS) & b1 is (SUBNETS) & b1 is (DIVERGENCE) & b1 is (ITERATED_LIMITS) holds
b1 is topological by Def25;
end;

theorem Th41: :: YELLOW_6:41
for T being non empty 1-sorted
for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )
proof
let T be non empty 1-sorted ; ::_thesis: for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )
let C be topological Convergence-Class of T; ::_thesis: for S being Subset of (ConvergenceSpace C) holds
( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )
let S be Subset of (ConvergenceSpace C); ::_thesis: ( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )
A1: the topology of (ConvergenceSpace C) =  {  V where V is Subset of T : for p being Element of T st p in V holds
for N being net of T st [N,p] in C holds
N is_eventually_in V  }  by Def24;
then A2: ( S in the topology of (ConvergenceSpace C) implies ex V being Subset of T st
( S = V & ( for p being Element of T st p in V holds
for N being net of T st [N,p] in C holds
N is_eventually_in V ) ) ) ;
 the carrier of (ConvergenceSpace C) = the carrier of T by Def24;
then  ( ( for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S ) implies S in the topology of (ConvergenceSpace C) ) by A1;
hence  ( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S ) by A2, PRE_TOPC:def_2; ::_thesis: verum
end;

theorem Th42: :: YELLOW_6:42
for T being non empty 1-sorted
for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is closed iff for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S )
proof
let T be non empty 1-sorted ; ::_thesis: for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is closed iff for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S )
let C be topological Convergence-Class of T; ::_thesis: for S being Subset of (ConvergenceSpace C) holds
( S is closed iff for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S )
let S be Subset of (ConvergenceSpace C); ::_thesis: ( S is closed iff for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S )
set CC = ConvergenceSpace C;
A1: the carrier of T = the carrier of (ConvergenceSpace C) by Def24;
hereby  ::_thesis: ( ( for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S ) implies S is closed )
assume  S is closed ; ::_thesis: for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S
then A2: S ` is open ;
let p be Element of T; ::_thesis: for N being net of T st [N,p] in C & N is_often_in S holds
p in S
let N be net of T; ::_thesis: ( [N,p] in C & N is_often_in S implies p in S )
assume A3: [N,p] in C ; ::_thesis: ( N is_often_in S implies p in S )
assume  N is_often_in S ; ::_thesis: p in S
then  not N is_eventually_in ([#] (ConvergenceSpace C)) \ S by A1, WAYBEL_0:10;
then  not p in S ` by A3, A2, Th41;
hence  p in S by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A4: for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S ; ::_thesis: S is closed
now__::_thesis:_for_p_being_Element_of_T_st_p_in_S_`_holds_
for_N_being_net_of_T_st_[N,p]_in_C_holds_
N_is_eventually_in_S_`
let p be Element of T; ::_thesis: ( p in S ` implies for N being net of T st [N,p] in C holds
N is_eventually_in S ` )
assume  p in S ` ; ::_thesis: for N being net of T st [N,p] in C holds
N is_eventually_in S `
then A5: not p in S by XBOOLE_0:def_5;
let N be net of T; ::_thesis: ( [N,p] in C implies N is_eventually_in S ` )
assume  [N,p] in C ; ::_thesis: N is_eventually_in S `
then  not N is_often_in S by A4, A5;
hence  N is_eventually_in S ` by A1, WAYBEL_0:10; ::_thesis: verum
end;
then  S ` is open by Th41;
hence  S is closed by TOPS_1:3; ::_thesis: verum
end;

theorem Th43: :: YELLOW_6:43
for T being non empty 1-sorted
for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C)
for p being Point of (ConvergenceSpace C) st p in Cl S holds
ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
proof
let T be non empty 1-sorted ; ::_thesis: for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C)
for p being Point of (ConvergenceSpace C) st p in Cl S holds
ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
let C be topological Convergence-Class of T; ::_thesis: for S being Subset of (ConvergenceSpace C)
for p being Point of (ConvergenceSpace C) st p in Cl S holds
ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
let S be Subset of (ConvergenceSpace C); ::_thesis: for p being Point of (ConvergenceSpace C) st p in Cl S holds
ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
let p be Point of (ConvergenceSpace C); ::_thesis: ( p in Cl S implies ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N ) )
assume A1: p in Cl S ; ::_thesis: ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
set CC = ConvergenceSpace C;
defpred S1[ Point of (ConvergenceSpace C)] means  ex N being net of ConvergenceSpace C st
( [N,$1] in C & rng the mapping of N c= S & $1 in Lim N );
set F =  {  q where q is Point of (ConvergenceSpace C) : S1[q]  }  ;
  {  q where q is Point of (ConvergenceSpace C) : S1[q]  }  is Subset of (ConvergenceSpace C) from DOMAIN_1:sch_7();
then reconsider F =  {  q where q is Point of (ConvergenceSpace C) : S1[q]  }  as Subset of (ConvergenceSpace C) ;
 for p being Element of T
for N being net of T st [N,p] in C & N is_often_in F holds
p in F
proof
let p be Element of T; ::_thesis: for N being net of T st [N,p] in C & N is_often_in F holds
p in F
reconsider q = p as Point of (ConvergenceSpace C) by Def24;
let N be net of T; ::_thesis: ( [N,p] in C & N is_often_in F implies p in F )
assume that
A2: [N,p] in C and
A3: N is_often_in F ; ::_thesis: p in F
 C c= [:(NetUniv T), the carrier of T:] by Def18;
then  N in NetUniv T by A2, ZFMISC_1:87;
then A4: ex N0 being strict net of T st
( N0 = N & the carrier of N0 in the_universe_of the carrier of T ) by Def11;
reconsider M = N " F as subnet of N by A3, Th22;
defpred S2[ Element of M, set ] means ( [$2,(M . $1)] in C & ex X being net of T st
( X = $2 & rng the mapping of X c= S ) );
A5: now__::_thesis:_for_i_being_Element_of_M_ex_x_being_set_st_S2[i,x]
let i be Element of M; ::_thesis: ex x being set st S2[i,x]
 i in the carrier of M ;
then  i in the mapping of N " F by Def10;
then A6: the mapping of N . i in F by FUNCT_2:38;
 the mapping of M = the mapping of N | the carrier of M by Def6;
then  the mapping of M . i in F by A6, FUNCT_1:49;
then consider q being Point of (ConvergenceSpace C) such that
A7: M . i = q and
A8: ex N being net of ConvergenceSpace C st
( [N,q] in C & rng the mapping of N c= S & q in Lim N ) ;
consider N being net of ConvergenceSpace C such that
A9: [N,q] in C and
A10: rng the mapping of N c= S and
 q in Lim N by A8;
reconsider x = N as set ;
take x = x; ::_thesis: S2[i,x]
thus  S2[i,x] ::_thesis: verum
proof
thus  [x,(M . i)] in C by A7, A9; ::_thesis: ex X being net of T st
( X = x & rng the mapping of X c= S )
reconsider X = N as net of T by Def24;
take  X ; ::_thesis: ( X = x & rng the mapping of X c= S )
thus  X = x ; ::_thesis: rng the mapping of X c= S
thus  rng the mapping of X c= S by A10; ::_thesis: verum
end;
end;
consider J being ManySortedSet of the carrier of M such that
A11: for i being Element of M holds S2[i,J . i] from PBOOLE:sch_6(A5);
 for i being set st i in the carrier of M holds
J . i is net of T
proof
let i be set ; ::_thesis: ( i in the carrier of M implies J . i is net of T )
assume  i in the carrier of M ; ::_thesis: J . i is net of T
then  ex X being net of T st
( X = J . i & rng the mapping of X c= S ) by A11;
hence  J . i is net of T ; ::_thesis: verum
end;
then reconsider J = J as net_set of the carrier of M,T by Th24;
set XX =  {  (rng the mapping of (J . i)) where i is Element of M : verum  }  ;
A12: for i being Element of M holds
( [(J . i),(M . i)] in C & rng the mapping of (J . i) c= S )
proof
let i be Element of M; ::_thesis: ( [(J . i),(M . i)] in C & rng the mapping of (J . i) c= S )
thus  [(J . i),(M . i)] in C by A11; ::_thesis: rng the mapping of (J . i) c= S
 ex X being net of T st
( X = J . i & rng the mapping of X c= S ) by A11;
hence  rng the mapping of (J . i) c= S ; ::_thesis: verum
end;
 for x being set st x in  {  (rng the mapping of (J . i)) where i is Element of M : verum  }  holds
x c= S
proof
let x be set ; ::_thesis: ( x in  {  (rng the mapping of (J . i)) where i is Element of M : verum  }  implies x c= S )
assume  x in  {  (rng the mapping of (J . i)) where i is Element of M : verum  }  ; ::_thesis: x c= S
then  ex i being Element of M st x = rng the mapping of (J . i) ;
hence  x c= S by A12; ::_thesis: verum
end;
then A13: union  {  (rng the mapping of (J . i)) where i is Element of M : verum  }  c= S by ZFMISC_1:76;
reconsider I = Iterated J as net of ConvergenceSpace C by Def24;
 rng the mapping of I c= union  {  (rng the mapping of (J . i)) where i is Element of M : verum  }  by Th28;
then A14: rng the mapping of I c= S by A13, XBOOLE_1:1;
 the carrier of M = the mapping of N " F by Def10;
then  the carrier of M in the_universe_of the carrier of T by A4, CLASSES1:def_1;
then  M in NetUniv T by Def11;
then  [M,p] in C by A2, Def21;
then A15: [I,p] in C by A12, Def23;
 C c= Convergence (ConvergenceSpace C) by Th40;
then  q in Lim I by A15, Def19;
hence  p in F by A15, A14; ::_thesis: verum
end;
then A16: F is closed by Th42;
 S c= F
proof
 {} in {{}} by TARSKI:def_1;
then reconsider r = {[{},{}]} as Relation of {{}} by RELSET_1:3;
set R = RelStr(# {{}},r #);
A17: now__::_thesis:_for_x,_y_being_Element_of_RelStr(#_{{}},r_#)_holds_x_<=_y
let x, y be Element of RelStr(# {{}},r #); ::_thesis: x <= y
 ( x = {} & y = {} ) by TARSKI:def_1;
then  [x,y] in {[{},{}]} by TARSKI:def_1;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
A18: RelStr(# {{}},r #) is transitive
proof
let x, y, z be Element of RelStr(# {{}},r #); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
thus  ( not x <= y or not y <= z or x <= z ) by A17; ::_thesis: verum
end;
 RelStr(# {{}},r #) is directed
proof
let x, y be Element of RelStr(# {{}},r #); :: according to YELLOW_6:def_3 ::_thesis: ex z being Element of RelStr(# {{}},r #) st
( x <= z & y <= z )
take  x ; ::_thesis: ( x <= x & y <= x )
thus  ( x <= x & y <= x ) by A17; ::_thesis: verum
end;
then reconsider R = RelStr(# {{}},r #) as non empty transitive directed RelStr by A18;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in F )
set V = the_universe_of the carrier of T;
assume A19: x in S ; ::_thesis: x in F
then reconsider q = x as Point of (ConvergenceSpace C) ;
set N = ConstantNet (R,q);
 the mapping of (ConstantNet (R,q)) = the carrier of (ConstantNet (R,q)) --> q by Def5;
then  rng the mapping of (ConstantNet (R,q)) = {q} by FUNCOP_1:8;
then A20: rng the mapping of (ConstantNet (R,q)) c= S by A19, ZFMISC_1:31;
 {} in the_universe_of the carrier of T by CLASSES2:56;
then A21: the carrier of R in the_universe_of the carrier of T by CLASSES2:2;
 the carrier of (ConvergenceSpace C) = the carrier of T by Def24;
then reconsider M = ConstantNet (R,q) as strict constant net of T by Lm6;
A22: the_value_of (ConstantNet (R,q)) = q by Th13;
then  the_value_of the mapping of M = q by Def8;
then A23: the_value_of M = q by Def8;
 RelStr(# the carrier of (ConstantNet (R,q)), the InternalRel of (ConstantNet (R,q)) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def5;
then  M in NetUniv T by A21, Def11;
then A24: [M,q] in C by A23, Def20;
 q in Lim (ConstantNet (R,q)) by A22, Th33;
hence  x in F by A24, A20; ::_thesis: verum
end;
then  Cl S c= F by A16, TOPS_1:5;
then  p in F by A1;
then  ex q being Point of (ConvergenceSpace C) st
( p = q & ex N being net of ConvergenceSpace C st
( [N,q] in C & rng the mapping of N c= S & q in Lim N ) ) ;
hence  ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N ) ; ::_thesis: verum
end;

theorem :: YELLOW_6:44
for T being non empty 1-sorted
for C being Convergence-Class of T holds
( Convergence (ConvergenceSpace C) = C iff C is topological )
proof
let T be non empty 1-sorted ; ::_thesis: for C being Convergence-Class of T holds
( Convergence (ConvergenceSpace C) = C iff C is topological )
let C be Convergence-Class of T; ::_thesis: ( Convergence (ConvergenceSpace C) = C iff C is topological )
set CC = ConvergenceSpace C;
set CCC = Convergence (ConvergenceSpace C);
A1: the carrier of (ConvergenceSpace C) = the carrier of T by Def24;
A2: for N being net of T
for n being net of ConvergenceSpace C st N = n holds
for x being subnet of n holds x is subnet of N
proof
let N be net of T; ::_thesis: for n being net of ConvergenceSpace C st N = n holds
for x being subnet of n holds x is subnet of N
let n be net of ConvergenceSpace C; ::_thesis: ( N = n implies for x being subnet of n holds x is subnet of N )
assume A3: N = n ; ::_thesis: for x being subnet of n holds x is subnet of N
let X be subnet of n; ::_thesis: X is subnet of N
reconsider x = X as net of T by Def24;
consider f being Function of X,n such that
A4: the mapping of X = the mapping of n * f and
A5: for m being Element of n ex n being Element of X st
for p being Element of X st n <= p holds
m <= f . p by Def9;
reconsider f = f as Function of x,N by A3;
 the mapping of x = the mapping of N * f by A3, A4;
hence  X is subnet of N by A3, A5, Def9; ::_thesis: verum
end;
A6: for N being net of T
for n being net of ConvergenceSpace C st N = n holds
for X being subnet of N holds X is subnet of n
proof
let N be net of T; ::_thesis: for n being net of ConvergenceSpace C st N = n holds
for X being subnet of N holds X is subnet of n
let n be net of ConvergenceSpace C; ::_thesis: ( N = n implies for X being subnet of N holds X is subnet of n )
assume A7: N = n ; ::_thesis: for X being subnet of N holds X is subnet of n
let X be subnet of N; ::_thesis: X is subnet of n
reconsider x = X as net of ConvergenceSpace C by Def24;
consider f being Function of X,N such that
A8: the mapping of X = the mapping of N * f and
A9: for m being Element of N ex n being Element of X st
for p being Element of X st n <= p holds
m <= f . p by Def9;
reconsider f = f as Function of x,n by A7;
 the mapping of x = the mapping of n * f by A7, A8;
hence  X is subnet of n by A7, A9, Def9; ::_thesis: verum
end;
A10: for N being net of T holds N is net of ConvergenceSpace C by Def24;
hereby  ::_thesis: ( C is topological implies Convergence (ConvergenceSpace C) = C )
assume A11: Convergence (ConvergenceSpace C) = C ; ::_thesis: C is topological
A12: C is (SUBNETS)
proof
let N be net of T; :: according to YELLOW_6:def_21 ::_thesis: for Y being subnet of N st Y in NetUniv T holds
for p being Element of T st [N,p] in C holds
[Y,p] in C
let Y be subnet of N; ::_thesis: ( Y in NetUniv T implies for p being Element of T st [N,p] in C holds
[Y,p] in C )
reconsider M = N as net of ConvergenceSpace C by Def24;
reconsider X = Y as subnet of M by A6;
assume  Y in NetUniv T ; ::_thesis: for p being Element of T st [N,p] in C holds
[Y,p] in C
then A13: X in NetUniv (ConvergenceSpace C) by A1, Lm7;
let p be Element of T; ::_thesis: ( [N,p] in C implies [Y,p] in C )
reconsider q = p as Element of (ConvergenceSpace C) by Def24;
assume  [N,p] in C ; ::_thesis: [Y,p] in C
then  [M,q] in Convergence (ConvergenceSpace C) by A11;
hence  [Y,p] in C by A11, A13, Def21; ::_thesis: verum
end;
A14: C is (ITERATED_LIMITS)
proof
let X be net of T; :: according to YELLOW_6:def_23 ::_thesis: for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C
let p be Element of T; ::_thesis: ( [X,p] in C implies for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C )
reconsider q = p as Element of (ConvergenceSpace C) by Def24;
reconsider x = X as net of ConvergenceSpace C by Def24;
assume A15: [X,p] in C ; ::_thesis: for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C
let J be net_set of the carrier of X,T; ::_thesis: ( ( for i being Element of X holds [(J . i),(X . i)] in C ) implies [(Iterated J),p] in C )
reconsider I = J as ManySortedSet of the carrier of x ;
 I is net_set of the carrier of x, ConvergenceSpace C
proof
let i be set ; :: according to YELLOW_6:def_12 ::_thesis: ( i in rng I implies i is net of ConvergenceSpace C )
assume  i in rng I ; ::_thesis: i is net of ConvergenceSpace C
then  i is net of T by Def12;
hence  i is net of ConvergenceSpace C by A10; ::_thesis: verum
end;
then reconsider I = J as net_set of the carrier of x, ConvergenceSpace C ;
assume A16: for i being Element of X holds [(J . i),(X . i)] in C ; ::_thesis: [(Iterated J),p] in C
now__::_thesis:_for_i_being_Element_of_x_holds_[(I_._i),(x_._i)]_in_Convergence_(ConvergenceSpace_C)
let i be Element of x; ::_thesis: [(I . i),(x . i)] in Convergence (ConvergenceSpace C)
reconsider j = i as Element of X ;
 X . j = x . i ;
hence  [(I . i),(x . i)] in Convergence (ConvergenceSpace C) by A11, A16; ::_thesis: verum
end;
then A17: [(Iterated I),q] in Convergence (ConvergenceSpace C) by A11, A15, Def23;
A18: RelStr(# the carrier of (Iterated I), the InternalRel of (Iterated I) #) = [:X,(product J):] by Def13
.= RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) by Def13 ;
A19: now__::_thesis:_for_j_being_set_st_j_in_dom_the_mapping_of_(Iterated_I)_holds_
the_mapping_of_(Iterated_I)_._j_=_the_mapping_of_(Iterated_J)_._j
let j be set ; ::_thesis: ( j in dom the mapping of (Iterated I) implies the mapping of (Iterated I) . j = the mapping of (Iterated J) . j )
assume  j in dom the mapping of (Iterated I) ; ::_thesis: the mapping of (Iterated I) . j = the mapping of (Iterated J) . j
then reconsider jj = j as Element of (Iterated I) ;
 the carrier of (Iterated I) = [: the carrier of x,(product (Carrier I)):] by Th26;
then consider j1 being Element of x, j2 being Element of product (Carrier I) such that
A20: jj = [j1,j2] by DOMAIN_1:1;
reconsider i1 = j1 as Element of X ;
reconsider j2 = j2 as Element of (product I) by YELLOW_1:def_4;
set i2 = j2;
 the carrier of (Iterated J) = [: the carrier of X,(product (Carrier J)):] by Th26;
then reconsider i = [i1,j2] as Element of (Iterated J) by ZFMISC_1:87;
thus  the mapping of (Iterated I) . j = (Iterated I) . jj
.= the mapping of (I . j1) . (j2 . j1) by A20, Th27
.= the mapping of (J . i1) . (j2 . i1)
.= (Iterated J) . i by Th27
.= the mapping of (Iterated J) . j by A20 ; ::_thesis: verum
end;
 dom the mapping of (Iterated I) = the carrier of (Iterated I) by FUNCT_2:def_1;
then  dom the mapping of (Iterated I) = dom the mapping of (Iterated J) by A18, FUNCT_2:def_1;
then  the mapping of (Iterated I) = the mapping of (Iterated J) by A19, FUNCT_1:2;
hence  [(Iterated J),p] in C by A11, A17, A18; ::_thesis: verum
end;
A21: C is (DIVERGENCE)
proof
let X be net of T; :: according to YELLOW_6:def_22 ::_thesis: for p being Element of T st X in NetUniv T & not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) )
let p be Element of T; ::_thesis: ( X in NetUniv T & not [X,p] in C implies ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) )
reconsider q = p as Element of (ConvergenceSpace C) by Def24;
reconsider x = X as net of ConvergenceSpace C by Def24;
assume  X in NetUniv T ; ::_thesis: ( [X,p] in C or ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) )
then A22: x in NetUniv (ConvergenceSpace C) by A1, Lm7;
assume  not [X,p] in C ; ::_thesis: ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) )
then consider y being subnet of x such that
A23: y in NetUniv (ConvergenceSpace C) and
A24: for z being subnet of y holds not [z,q] in Convergence (ConvergenceSpace C) by A11, A22, Def22;
reconsider Y = y as subnet of X by A2;
take  Y ; ::_thesis: ( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) )
thus  Y in NetUniv T by A1, A23, Lm7; ::_thesis: for Z being subnet of Y holds not [Z,p] in C
let Z be subnet of Y; ::_thesis: not [Z,p] in C
reconsider z = Z as subnet of y by A6;
 not [z,q] in Convergence (ConvergenceSpace C) by A24;
hence  not [Z,p] in C by A11; ::_thesis: verum
end;
 C is (CONSTANTS)
proof
let N be constant net of T; :: according to YELLOW_6:def_20 ::_thesis: ( N in NetUniv T implies [N,(the_value_of N)] in C )
reconsider M = N as net of ConvergenceSpace C by Def24;
 the mapping of N is constant ;
then  the mapping of M is constant ;
then reconsider M = M as constant net of ConvergenceSpace C by Def4;
assume  N in NetUniv T ; ::_thesis: [N,(the_value_of N)] in C
then A25: M in NetUniv (ConvergenceSpace C) by A1, Lm7;
the_value_of M = the_value_of the mapping of M by Def8
.= the_value_of the mapping of N
.= the_value_of N by Def8 ;
hence  [N,(the_value_of N)] in C by A11, A25, Def20; ::_thesis: verum
end;
hence  C is topological by A12, A21, A14; ::_thesis: verum
end;
assume A26: ( C is (CONSTANTS) & C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) ) ; :: according to YELLOW_6:def_25 ::_thesis: Convergence (ConvergenceSpace C) = C
then reconsider C9 = C as topological Convergence-Class of T ;
A27: Convergence (ConvergenceSpace C) c= C
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in Convergence (ConvergenceSpace C) or [x,b1] in C )
let y be set ; ::_thesis: ( not [x,y] in Convergence (ConvergenceSpace C) or [x,y] in C )
assume A28: [x,y] in Convergence (ConvergenceSpace C) ; ::_thesis: [x,y] in C
 Convergence (ConvergenceSpace C) c= [:(NetUniv (ConvergenceSpace C)), the carrier of (ConvergenceSpace C):] by Def18;
then consider M being Element of NetUniv (ConvergenceSpace C), p being Element of (ConvergenceSpace C) such that
A29: [x,y] = [M,p] by A28, DOMAIN_1:1;
reconsider q = p as Point of T by Def24;
A30: M in NetUniv (ConvergenceSpace C) ;
A31: ex N being strict net of ConvergenceSpace C st
( N = M & the carrier of N in the_universe_of the carrier of (ConvergenceSpace C) ) by Def11;
assume A32: not [x,y] in C ; ::_thesis: contradiction
reconsider M = M as net of ConvergenceSpace C by A31;
reconsider N = M as net of T by Def24;
 N in NetUniv T by A1, A30, Lm7;
then consider Y being subnet of N such that
A33: Y in NetUniv T and
A34: for Z being subnet of Y holds not [Z,q] in C by A26, A29, A32, Def22;
reconsider Y9 = Y as subnet of M by A6;
reconsider YY = RelStr(# the carrier of Y, the InternalRel of Y #) as non empty transitive directed RelStr by Lm1, Lm2;
set X = ConstantNet (YY,q);
defpred S1[ set , set ] means  ex i being Element of Y ex Ji being net of T st
( $1 = i & Ji = $2 & [Ji,p] in C & rng the mapping of Ji c=  {  (Y . c) where c is Element of Y : i <= c  }  );
A35: RelStr(# the carrier of (ConstantNet (YY,q)), the InternalRel of (ConstantNet (YY,q)) #) = YY by Def5;
reconsider X = ConstantNet (YY,q) as strict constant net of T ;
A36: p in Lim M by A28, A29, Def19;
A37: for x being set st x in the carrier of X holds
ex j being set st S1[x,j]
proof
let x be set ; ::_thesis: ( x in the carrier of X implies ex j being set st S1[x,j] )
assume  x in the carrier of X ; ::_thesis: ex j being set st S1[x,j]
then reconsider i9 = x as Element of Y9 by Th4;
reconsider i = i9 as Element of Y ;
 Lim M c= Lim Y9 by Th32;
then consider S being Subset of (ConvergenceSpace C) such that
A38: S =  {  (Y9 . c) where c is Element of Y9 : i9 <= c  }  and
A39: p in Cl S by A36, Th34;
consider Go being net of ConvergenceSpace C9 such that
A40: [Go,p] in C9 and
A41: rng the mapping of Go c= S and
 p in Lim Go by A39, Th43;
reconsider Ji = Go as net of T by Def24;
take  Ji ; ::_thesis: S1[x,Ji]
take  i ; ::_thesis: ex Ji being net of T st
( x = i & Ji = Ji & [Ji,p] in C & rng the mapping of Ji c=  {  (Y . c) where c is Element of Y : i <= c  }  )
take  Ji ; ::_thesis: ( x = i & Ji = Ji & [Ji,p] in C & rng the mapping of Ji c=  {  (Y . c) where c is Element of Y : i <= c  }  )
thus  ( x = i & Ji = Ji & [Ji,p] in C ) by A40; ::_thesis: rng the mapping of Ji c=  {  (Y . c) where c is Element of Y : i <= c  }
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng the mapping of Ji or e in  {  (Y . c) where c is Element of Y : i <= c  }  )
assume  e in rng the mapping of Ji ; ::_thesis: e in  {  (Y . c) where c is Element of Y : i <= c  }
then  e in S by A41;
then consider c9 being Element of Y9 such that
A42: e = Y9 . c9 and
A43: i9 <= c9 by A38;
reconsider cc = c9 as Element of Y ;
 e = Y . cc by A42;
hence  e in  {  (Y . c) where c is Element of Y : i <= c  }  by A43; ::_thesis: verum
end;
consider J being ManySortedSet of the carrier of X such that
A44: for x being set st x in the carrier of X holds
S1[x,J . x] from PBOOLE:sch_3(A37);
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_X_holds_
J_._x_is_net_of_T
let x be set ; ::_thesis: ( x in the carrier of X implies J . x is net of T )
assume  x in the carrier of X ; ::_thesis: J . x is net of T
then  ex i being Element of Y ex Ji being net of T st
( x = i & Ji = J . x & [Ji,p] in C & rng the mapping of Ji c=  {  (Y . c) where c is Element of Y : i <= c  }  ) by A44;
hence  J . x is net of T ; ::_thesis: verum
end;
then reconsider J = J as yielding_non-empty_carriers net_set of the carrier of X,T by Th24;
reconsider X9 = X as net of ConvergenceSpace C by Def24;
A45: the mapping of X9 is constant ;
A46: for i being Element of X holds [(J . i),(X . i)] in C
proof
let i be Element of X; ::_thesis: [(J . i),(X . i)] in C
 ex ii being Element of Y ex Ji being net of T st
( i = ii & Ji = J . i & [Ji,p] in C & rng the mapping of Ji c=  {  (Y . c) where c is Element of Y : ii <= c  }  ) by A44;
hence  [(J . i),(X . i)] in C by Th5; ::_thesis: verum
end;
A47: the_value_of X = q by Th13;
reconsider X9 = X9 as constant net of ConvergenceSpace C by A45, Def4;
A48: RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = [:X,(product J):] by Def13;
then A49: the carrier of (Iterated J) = [: the carrier of X, the carrier of (product J):] by YELLOW_3:def_2;
A50: Iterated J is subnet of Y
proof
set F = the Element of (product J);
set h = the mapping of (Iterated J);
set g = the mapping of Y9;
defpred S2[ set , set , set ] means  ex f being Function ex x being Element of X st
( f . $2 = $1 & x = $3 & the mapping of (J . x) . $2 = the mapping of Y . $1 );
deffunc H1( Element of Y) ->  set =  {  c where c is Element of Y : $1 <= c  }  ;
consider B being ManySortedSet of the carrier of Y such that
A51: for i being Element of Y holds B . i = H1(i) from PBOOLE:sch_5();
now__::_thesis:_not_{}_in_rng_B
assume  {} in rng B ; ::_thesis: contradiction
then consider i being set  such that
A52: i in dom B and
A53: B . i = {} by FUNCT_1:def_3;
reconsider i = i as Element of Y by A52;
consider j being Element of Y such that
A54: i <= j and
 i <= j by Def3;
 j in  {  c where c is Element of Y : i <= c  }  by A54;
hence  contradiction by A51, A53; ::_thesis: verum
end;
then reconsider B = B as V2() ManySortedSet of the carrier of Y by RELAT_1:def_9;
deffunc H2( Element of X) ->  set = the carrier of (J . $1);
consider M being ManySortedSet of the carrier of X such that
A55: for x being Element of X holds M . x = H2(x) from PBOOLE:sch_5();
reconsider B9 = B as V2() ManySortedSet of the carrier of X by A35;
A56: for i being set st i in the carrier of X holds
for x being set st x in M . i holds
ex y being set st
( y in B9 . i & S2[y,x,i] )
proof
let i be set ; ::_thesis: ( i in the carrier of X implies for x being set st x in M . i holds
ex y being set st
( y in B9 . i & S2[y,x,i] ) )
assume A57: i in the carrier of X ; ::_thesis: for x being set st x in M . i holds
ex y being set st
( y in B9 . i & S2[y,x,i] )
consider e being Element of Y, Ji being net of T such that
A58: i = e and
A59: Ji = J . i and
 [Ji,p] in C and
A60: rng the mapping of Ji c=  {  (Y . c) where c is Element of Y : e <= c  }  by A44, A57;
reconsider i9 = i as Element of X by A57;
defpred S3[ set , set ] means  the mapping of Ji . $1 = the mapping of Y . $2;
A61: for ji being Element of Ji ex u being Element of B9 . i9 st S3[ji,u]
proof
let ji be Element of Ji; ::_thesis: ex u being Element of B9 . i9 st S3[ji,u]
 ji in the carrier of Ji ;
then  ji in dom the mapping of Ji by FUNCT_2:def_1;
then  the mapping of Ji . ji in rng the mapping of Ji by FUNCT_1:def_3;
then  the mapping of Ji . ji in  {  (Y . c) where c is Element of Y : e <= c  }  by A60;
then consider c being Element of Y such that
A62: the mapping of Ji . ji = Y . c and
A63: e <= c ;
 c in  {  cc where cc is Element of Y : e <= cc  }  by A63;
then reconsider c = c as Element of B9 . i9 by A51, A58;
take  c ; ::_thesis: S3[ji,c]
thus  the mapping of Ji . ji = the mapping of Y . c by A62; ::_thesis: verum
end;
consider f being Function of the carrier of Ji,(B9 . i9) such that
A64: for ji being Element of Ji holds S3[ji,f . ji] from FUNCT_2:sch_3(A61);
let x be set ; ::_thesis: ( x in M . i implies ex y being set st
( y in B9 . i & S2[y,x,i] ) )
assume  x in M . i ; ::_thesis: ex y being set st
( y in B9 . i & S2[y,x,i] )
then reconsider ji = x as Element of Ji by A55, A57, A59;
reconsider f = f as Function of the carrier of Ji,(B . i) ;
take  f . x ; ::_thesis: ( f . x in B9 . i & S2[f . x,x,i] )
 f . ji in B . i ;
hence  f . x in B9 . i ; ::_thesis: S2[f . x,x,i]
take  f ; ::_thesis: ex x being Element of X st
( f . x = f . x & x = i & the mapping of (J . x) . x = the mapping of Y . (f . x) )
take  i9 ; ::_thesis: ( f . x = f . x & i9 = i & the mapping of (J . i9) . x = the mapping of Y . (f . x) )
thus  ( f . x = f . x & i9 = i ) ; ::_thesis: the mapping of (J . i9) . x = the mapping of Y . (f . x)
thus  the mapping of (J . i9) . x = the mapping of Ji . ji by A59
.= the mapping of Y . (f . x) by A64 ; ::_thesis: verum
end;
consider u being ManySortedFunction of M,B9 such that
A65: for i being set st i in the carrier of X holds
ex f being Function of (M . i),(B9 . i) st
( f = u . i & ( for x being set st x in M . i holds
S2[f . x,x,i] ) ) from MSSUBFAM:sch_1(A56);
deffunc H3( Element of X, Element of (product J)) ->  set = (u . $1) . ($2 . $1);
A66: for x being Element of X
for y being Element of (product J) holds H3(x,y) in the carrier of Y
proof
let x be Element of X; ::_thesis: for y being Element of (product J) holds H3(x,y) in the carrier of Y
let y be Element of (product J); ::_thesis: H3(x,y) in the carrier of Y
reconsider x9 = x as Element of X9 ;
reconsider k = x as Element of Y by A35;
defpred S3[ Element of Y] means k <= $1;
set ZZ =  {  c where c is Element of Y : S3[c]  }  ;
A67:  {  c where c is Element of Y : S3[c]  }  is Subset of Y from DOMAIN_1:sch_7();
 x9 in the carrier of X9 ;
then A68: x9 in dom (Carrier J) by PARTFUN1:def_2;
 y in the carrier of (product J) ;
then  y in product (Carrier J) by YELLOW_1:def_4;
then  y . x9 in (Carrier J) . x9 by A68, CARD_3:9;
then  y . x9 in the carrier of (J . x) by Th2;
then  ( u . k is Function of (M . k),(B . k) & y . x in M . k ) by A55, PBOOLE:def_15;
then A69: (u . k) . (y . x) in B . k by FUNCT_2:5;
 B . k =  {  c where c is Element of Y : S3[c]  }  by A51;
hence  H3(x,y) in the carrier of Y by A67, A69; ::_thesis: verum
end;
consider f being Function of [: the carrier of X, the carrier of (product J):], the carrier of Y such that
A70: for x being Element of X
for y being Element of (product J) holds f . (x,y) = H3(x,y) from FUNCT_7:sch_1(A66);
reconsider f = f as Function of (Iterated J),Y by A49;
A71: for x being Element of X
for j being Element of M . x holds the mapping of (J . x) . j = the mapping of Y . ((u . x) . j)
proof
let i be Element of X; ::_thesis: for j being Element of M . i holds the mapping of (J . i) . j = the mapping of Y . ((u . i) . j)
let j be Element of M . i; ::_thesis: the mapping of (J . i) . j = the mapping of Y . ((u . i) . j)
consider f being Function of (M . i),(B9 . i) such that
A72: f = u . i and
A73: for x being set st x in M . i holds
S2[f . x,x,i] by A65;
 M . i = the carrier of (J . i) by A55;
then  S2[f . j,j,i] by A73;
hence  the mapping of (J . i) . j = the mapping of Y . ((u . i) . j) by A72; ::_thesis: verum
end;
A74: for x being set st x in dom the mapping of (Iterated J) holds
the mapping of (Iterated J) . x = the mapping of Y9 . (f . x)
proof
let x be set ; ::_thesis: ( x in dom the mapping of (Iterated J) implies the mapping of (Iterated J) . x = the mapping of Y9 . (f . x) )
assume  x in dom the mapping of (Iterated J) ; ::_thesis: the mapping of (Iterated J) . x = the mapping of Y9 . (f . x)
then  x in the carrier of (Iterated J) ;
then  x in [: the carrier of X9,(product (Carrier J)):] by Th26;
then  x in [: the carrier of X9, the carrier of (product J):] by YELLOW_1:def_4;
then consider x1 being Element of X9, x2 being Element of (product J) such that
A75: x = [x1,x2] by DOMAIN_1:1;
reconsider x9 = x1 as Element of X ;
 x2 in the carrier of (product J) ;
then A76: x2 in product (Carrier J) by YELLOW_1:def_4;
 ( dom (Carrier J) = the carrier of X9 & the carrier of (J . x9) = (Carrier J) . x1 ) by Th2, PARTFUN1:def_2;
then  x2 . x1 in the carrier of (J . x9) by A76, CARD_3:9;
then reconsider j = x2 . x1 as Element of M . x9 by A55;
thus  the mapping of (Iterated J) . x = the mapping of (Iterated J) . (x1,x2) by A75
.= the mapping of (J . x9) . (x2 . x1) by Def13
.= the mapping of Y9 . ((u . x9) . j) by A71
.= the mapping of Y9 . (f . (x1,x2)) by A70
.= the mapping of Y9 . (f . x) by A75 ; ::_thesis: verum
end;
take  f ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of (Iterated J) = the mapping of Y * f & ( for m being Element of Y ex n being Element of (Iterated J) st
for p being Element of (Iterated J) st n <= p holds
m <= f . p ) )
 for x being set holds
( x in dom the mapping of (Iterated J) iff ( x in dom f & f . x in dom the mapping of Y9 ) )
proof
let x be set ; ::_thesis: ( x in dom the mapping of (Iterated J) iff ( x in dom f & f . x in dom the mapping of Y9 ) )
hereby  ::_thesis: ( x in dom f & f . x in dom the mapping of Y9 implies x in dom the mapping of (Iterated J) )
assume  x in dom the mapping of (Iterated J) ; ::_thesis: ( x in dom f & f . x in dom the mapping of Y9 )
then  x in the carrier of (Iterated J) ;
then  x in [: the carrier of X9,(product (Carrier J)):] by Th26;
then A77: x in [: the carrier of X9, the carrier of (product J):] by YELLOW_1:def_4;
hence  x in dom f by FUNCT_2:def_1; ::_thesis: f . x in dom the mapping of Y9
 f . x in the carrier of Y by A77, FUNCT_2:5;
hence  f . x in dom the mapping of Y9 by FUNCT_2:def_1; ::_thesis: verum
end;
assume that
A78: x in dom f and
 f . x in dom the mapping of Y9 ; ::_thesis: x in dom the mapping of (Iterated J)
 x in [: the carrier of X9, the carrier of (product J):] by A78, FUNCT_2:def_1;
then  x in [: the carrier of X9,(product (Carrier J)):] by YELLOW_1:def_4;
then  x in the carrier of (Iterated J) by Th26;
hence  x in dom the mapping of (Iterated J) by FUNCT_2:def_1; ::_thesis: verum
end;
hence  the mapping of (Iterated J) = the mapping of Y * f by A74, FUNCT_1:10; ::_thesis: for m being Element of Y ex n being Element of (Iterated J) st
for p being Element of (Iterated J) st n <= p holds
m <= f . p
let m be Element of Y; ::_thesis: ex n being Element of (Iterated J) st
for p being Element of (Iterated J) st n <= p holds
m <= f . p
reconsider n = [m, the Element of (product J)] as Element of (Iterated J) by A35, A49, ZFMISC_1:87;
take  n ; ::_thesis: for p being Element of (Iterated J) st n <= p holds
m <= f . p
let p be Element of (Iterated J); ::_thesis: ( n <= p implies m <= f . p )
consider k9 being Element of X, G being Element of (product J) such that
A79: p = [k9,G] by A49, DOMAIN_1:1;
reconsider m9 = m as Element of X by A35;
reconsider F = the Element of (product J) as Element of (product J) ;
 G in the carrier of (product J) ;
then A80: ( dom (Carrier J) = the carrier of X9 & G in product (Carrier J) ) by PARTFUN1:def_2, YELLOW_1:def_4;
reconsider k = k9 as Element of Y by A35;
A81: f . (k9,G) = (u . k) . (G . k) by A70;
reconsider k99 = k9 as Element of X9 ;
A82: u . k is Function of (M . k),(B . k) by PBOOLE:def_15;
then A83: rng (u . k) c= B . k by RELAT_1:def_19;
dom (u . k) = M . k by A82, FUNCT_2:def_1
.= the carrier of (J . k9) by A55
.= (Carrier J) . k99 by Th2 ;
then A84: G . k99 in dom (u . k) by A80, CARD_3:9;
reconsider k9 = k as Element of X ;
reconsider G = G as Element of (product J) ;
assume  n <= p ; ::_thesis: m <= f . p
then  [m9,F] <= [k9,G] by A48, A79, Lm3;
then  m9 <= k9 by YELLOW_3:11;
then A85: m <= k by A35, Lm3;
 f . p in rng (u . k) by A79, A81, A84, FUNCT_1:def_3;
then  f . p in B . k by A83;
then  f . p in  {  c where c is Element of Y : k <= c  }  by A51;
then  ex c being Element of Y st
( c = f . p & k <= c ) ;
hence  m <= f . p by A85, YELLOW_0:def_2; ::_thesis: verum
end;
A86: RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of Y, the InternalRel of Y #) by Def5;
 ex N0 being strict net of T st
( N0 = Y & the carrier of N0 in the_universe_of the carrier of T ) by A33, Def11;
then  X in NetUniv T by A86, Def11;
then  [X,q] in C by A26, A47, Def20;
then  [(Iterated J),q] in C by A26, A46, Def23;
hence  contradiction by A34, A50; ::_thesis: verum
end;
 C c= Convergence (ConvergenceSpace C) by Th40;
hence  Convergence (ConvergenceSpace C) = C by A27, XBOOLE_0:def_10; ::_thesis: verum
end;