:: YELLOW_6 semantic presentation

definition
let c1 be Function;
assume E1: ( not c1 is empty & c1 is constant ) ;
func the_value_of c1 -> set means :Def1: :: YELLOW_6:def 1
ex b1 being set st
( b1 in dom a1 & a2 = a1 . b1 );
existence
ex b1 being set ex b2 being set st
( b2 in dom c1 & b1 = c1 . b2 )
proof end;
uniqueness
for b1, b2 being set st ex b3 being set st
( b3 in dom c1 & b1 = c1 . b3 ) & ex b3 being set st
( b3 in dom c1 & b2 = c1 . b3 ) holds
b1 = b2 by E1, SEQM_3:def 5;
end;

:: deftheorem Def1 defines the_value_of YELLOW_6:def 1 :
for b1 being Function st not b1 is empty & b1 is constant holds
for b2 being set holds
( b2 = the_value_of b1 iff ex b3 being set st
( b3 in dom b1 & b2 = b1 . b3 ) );

registration
cluster non empty constant set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is constant )
proof end;
end;

theorem Th1: :: YELLOW_6:1
canceled;

theorem Th2: :: YELLOW_6:2
for b1 being non empty set
for b2 being set holds the_value_of (b1 --> b2) = b2
proof end;

registration
cluster universal -> epsilon-transitive being_Tarski-Class set ;
coherence
for b1 being set st b1 is universal holds
( b1 is epsilon-transitive & b1 is being_Tarski-Class ) by CLASSES2:def 1;
cluster epsilon-transitive being_Tarski-Class -> universal set ;
coherence
for b1 being set st b1 is epsilon-transitive & b1 is being_Tarski-Class holds
b1 is universal by CLASSES2:def 1;
end;

definition
let c1 be set ;
canceled;
func the_universe_of c1 -> set equals :: YELLOW_6:def 3
 Tarski-Class (the_transitive-closure_of a1);
correctness
coherence
Tarski-Class (the_transitive-closure_of c1) is set ;
;
end;

:: deftheorem Def2 YELLOW_6:def 2 :
canceled;

:: deftheorem Def3 defines the_universe_of YELLOW_6:def 3 :
for b1 being set holds the_universe_of b1 = Tarski-Class (the_transitive-closure_of b1);

registration
let c1 be set ;
cluster the_universe_of a1 -> epsilon-transitive being_Tarski-Class universal ;
coherence
( the_universe_of c1 is epsilon-transitive & the_universe_of c1 is being_Tarski-Class ) ;
end;

registration
let c1 be set ;
cluster the_universe_of a1 -> non empty epsilon-transitive being_Tarski-Class universal ;
coherence
( the_universe_of c1 is universal & not the_universe_of c1 is empty ) ;
end;

theorem Th3: :: YELLOW_6:3
canceled;

theorem Th4: :: YELLOW_6:4
canceled;

theorem Th5: :: YELLOW_6:5
for b1 being Universe
for b2 being Function st dom b2 in b1 & rng b2 c= b1 holds
product b2 in b1
proof end;

theorem Th6: :: YELLOW_6:6
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being Point of b1 holds
( b3 in Cl b2 iff for b4 being a_neighborhood of b3 holds b4 meets b2 )
proof end;

theorem Th7: :: YELLOW_6:7
for b1 being non empty TopSpace
for b2 being Subset of b1 holds [#] b1 is a_neighborhood of b2
proof end;

theorem Th8: :: YELLOW_6:8
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being a_neighborhood of b2 holds b2 c= b3
proof end;

theorem Th9: :: YELLOW_6:9
for b1 being non empty set
for b2 being 1-sorted-yielding ManySortedSet of b1
for b3 being Element of b1 holds (Carrier b2) . b3 = the carrier of (b2 . b3)
proof end;

registration
cluster non empty constant 1-sorted-yielding set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is constant & b1 is 1-sorted-yielding )
proof end;
end;

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

definition
let c1 be 1-sorted-yielding Function;
redefine attr a1 is non-Empty means :Def4: :: YELLOW_6:def 4
for b1 being set st b1 in rng a1 holds
b1 is non empty 1-sorted ;
compatibility
( c1 is yielding_non-empty_carriers iff for b1 being set st b1 in rng c1 holds
b1 is non empty 1-sorted )
proof end;
end;

:: deftheorem Def4 defines yielding_non-empty_carriers YELLOW_6:def 4 :
for b1 being 1-sorted-yielding Function holds
( b1 is yielding_non-empty_carriers iff for b2 being set st b2 in rng b1 holds
b2 is non empty 1-sorted );

registration
let c1 be set ;
let c2 be 1-sorted ;
cluster K192(a1,a2) -> 1-sorted-yielding ;
coherence
c1 --> c2 is 1-sorted-yielding
proof end;
end;

registration
let c1 be set ;
cluster 1-sorted-yielding yielding_non-empty_carriers ManySortedSet of a1;
existence
ex b1 being 1-sorted-yielding ManySortedSet of c1 st b1 is yielding_non-empty_carriers
proof end;
end;

registration
let c1 be non empty set ;
let c2 be RelStr-yielding ManySortedSet of c1;
cluster the carrier of (product a2) -> functional ;
coherence
the carrier of (product c2) is functional
proof end;
end;

registration
let c1 be set ;
let c2 be 1-sorted-yielding yielding_non-empty_carriers ManySortedSet of c1;
cluster Carrier a2 -> V3 ;
coherence
Carrier c2 is non-empty
proof end;
end;

theorem Th10: :: YELLOW_6:10
for b1 being non empty 1-sorted
for b2 being Subset of b1
for b3 being Element of b1 holds
( not b3 in b2 iff b3 in b2 ` ) by SUBSET_1:50, SUBSET_1:54;

registration
let c1 be non empty RelStr ;
let c2 be lower Subset of c1;
cluster a2 ` -> upper ;
coherence
c2 ` is upper
proof end;
end;

registration
let c1 be non empty RelStr ;
let c2 be upper Subset of c1;
cluster a2 ` -> lower ;
coherence
c2 ` is lower
proof end;
end;

definition
let c1 be non empty RelStr ;
redefine attr a1 is directed means :Def5: :: YELLOW_6:def 5
for b1, b2 being Element of a1 ex b3 being Element of a1 st
( b1 <= b3 & b2 <= b3 );
compatibility
( c1 is directed iff for b1, b2 being Element of c1 ex b3 being Element of c1 st
( b1 <= b3 & b2 <= b3 ) )
proof end;
end;

:: deftheorem Def5 defines directed YELLOW_6:def 5 :
for b1 being non empty RelStr holds
( b1 is directed iff for b2, b3 being Element of b1 ex b4 being Element of b1 st
( b2 <= b4 & b3 <= b4 ) );

registration
let c1 be set ;
cluster BoolePoset a1 -> directed ;
coherence
BoolePoset c1 is directed
proof end;
end;

registration
cluster non empty strict transitive directed RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is directed & b1 is transitive & b1 is strict )
proof end;
end;

Lemma9: for b1 being non empty RelStr holds
( b1 is directed iff RelStr(# the carrier of b1,the InternalRel of b1 #) is directed )
proof end;

Lemma10: for b1 being non empty RelStr holds
( b1 is transitive iff RelStr(# the carrier of b1,the InternalRel of b1 #) is transitive )
proof end;

definition
let c1 be non empty set ;
let c2 be non empty RelStr ;
let c3 be Function of c1,the carrier of c2;
let c4 be Element of c1;
redefine func . as c3 . c4 -> Element of a2;
coherence
c3 . c4 is Element of c2
proof end;
end;

registration
let c1 be set ;
cluster RelStr-yielding yielding_non-empty_carriers ManySortedSet of a1;
existence
ex b1 being RelStr-yielding ManySortedSet of c1 st b1 is yielding_non-empty_carriers
proof end;
end;

registration
let c1 be non empty set ;
let c2 be RelStr-yielding yielding_non-empty_carriers ManySortedSet of c1;
cluster product a2 -> non empty ;
coherence
not product c2 is empty
proof end;
end;

theorem Th11: :: YELLOW_6:11
for b1, b2 being RelStr holds [#] [:b1,b2:] = [:([#] b1),([#] b2):] by YELLOW_3:def 2;

registration
let c1, c2 be directed RelStr ;
cluster [:a1,a2:] -> directed ;
coherence
[:c1,c2:] is directed
proof end;
end;

theorem Th12: :: YELLOW_6:12
for b1 being RelStr holds the carrier of b1 = the carrier of (b1 ~ )
proof end;

Lemma13: for b1, b2 being RelStr
for b3, b4 being Element of b1
for b5, b6 being Element of b2 st b3 = b5 & b4 = b6 & RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of b2,the InternalRel of b2 #) & b3 <= b4 holds
b5 <= b6
proof end;

definition
let c1 be 1-sorted ;
let c2 be NetStr of c1;
attr a2 is constant means :Def6: :: YELLOW_6:def 6
the mapping of a2 is constant;
end;

:: deftheorem Def6 defines constant YELLOW_6:def 6 :
for b1 being 1-sorted
for b2 being NetStr of b1 holds
( b2 is constant iff the mapping of b2 is constant );

definition
let c1 be RelStr ;
let c2 be non empty 1-sorted ;
let c3 be Element of c2;
func c1 --> c3 -> strict NetStr of a2 means :Def7: :: YELLOW_6:def 7
( RelStr(# the carrier of a4,the InternalRel of a4 #) = RelStr(# the carrier of a1,the InternalRel of a1 #) & the mapping of a4 = the carrier of a4 --> a3 );
existence
ex b1 being strict NetStr of c2 st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of c1,the InternalRel of c1 #) & the mapping of b1 = the carrier of b1 --> c3 )
proof end;
correctness
uniqueness
for b1, b2 being strict NetStr of c2 st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of c1,the InternalRel of c1 #) & the mapping of b1 = the carrier of b1 --> c3 & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of c1,the InternalRel of c1 #) & the mapping of b2 = the carrier of b2 --> c3 holds
b1 = b2;
;
end;

:: deftheorem Def7 defines --> YELLOW_6:def 7 :
for b1 being RelStr
for b2 being non empty 1-sorted
for b3 being Element of b2
for b4 being strict NetStr of b2 holds
( b4 = b1 --> b3 iff ( RelStr(# the carrier of b4,the InternalRel of b4 #) = RelStr(# the carrier of b1,the InternalRel of b1 #) & the mapping of b4 = the carrier of b4 --> b3 ) );

registration
let c1 be RelStr ;
let c2 be non empty 1-sorted ;
let c3 be Element of c2;
cluster a1 --> a3 -> strict constant ;
coherence
c1 --> c3 is constant
proof end;
end;

registration
let c1 be non empty RelStr ;
let c2 be non empty 1-sorted ;
let c3 be Element of c2;
cluster a1 --> a3 -> non empty strict constant ;
coherence
not c1 --> c3 is empty
proof end;
end;

registration
let c1 be non empty directed RelStr ;
let c2 be non empty 1-sorted ;
let c3 be Element of c2;
cluster a1 --> a3 -> non empty strict directed constant ;
coherence
c1 --> c3 is directed
proof end;
end;

registration
let c1 be non empty transitive RelStr ;
let c2 be non empty 1-sorted ;
let c3 be Element of c2;
cluster a1 --> a3 -> non empty transitive strict constant ;
coherence
c1 --> c3 is transitive
proof end;
end;

theorem Th13: :: YELLOW_6:13
for b1 being RelStr
for b2 being non empty 1-sorted
for b3 being Element of b2 holds the carrier of (b1 --> b3) = the carrier of b1
proof end;

theorem Th14: :: YELLOW_6:14
for b1 being non empty RelStr
for b2 being non empty 1-sorted
for b3 being Element of b2
for b4 being Element of (b1 --> b3) holds (b1 --> b3) . b4 = b3
proof end;

registration
let c1 be non empty 1-sorted ;
let c2 be non empty NetStr of c1;
cluster the mapping of a2 -> non empty ;
coherence
not the mapping of c2 is empty by FUNCT_2:def 1, RELAT_1:60;
end;

theorem Th15: :: YELLOW_6:15
for b1 being RelStr holds b1 is full SubRelStr of b1
proof end;

theorem Th16: :: YELLOW_6:16
for b1 being RelStr
for b2 being SubRelStr of b1
for b3 being SubRelStr of b2 holds b3 is SubRelStr of b1
proof end;

definition
let c1 be 1-sorted ;
let c2 be NetStr of c1;
mode SubNetStr of c2 -> NetStr of a1 means :Def8: :: YELLOW_6:def 8
( a3 is SubRelStr of a2 & the mapping of a3 = the mapping of a2 | the carrier of a3 );
existence
ex b1 being NetStr of c1 st
( b1 is SubRelStr of c2 & the mapping of b1 = the mapping of c2 | the carrier of b1 )
proof end;
end;

:: deftheorem Def8 defines SubNetStr YELLOW_6:def 8 :
for b1 being 1-sorted
for b2, b3 being NetStr of b1 holds
( b3 is SubNetStr of b2 iff ( b3 is SubRelStr of b2 & the mapping of b3 = the mapping of b2 | the carrier of b3 ) );

theorem Th17: :: YELLOW_6:17
for b1 being 1-sorted
for b2 being NetStr of b1 holds b2 is SubNetStr of b2
proof end;

theorem Th18: :: YELLOW_6:18
for b1 being 1-sorted
for b2 being NetStr of b1
for b3 being SubNetStr of b2
for b4 being SubNetStr of b3 holds b4 is SubNetStr of b2
proof end;

Lemma21: for b1 being 1-sorted
for b2 being NetStr of b1 holds NetStr(# the carrier of b2,the InternalRel of b2,the mapping of b2 #) is SubNetStr of b2
proof end;

definition
let c1 be 1-sorted ;
let c2 be NetStr of c1;
let c3 be SubNetStr of c2;
attr a3 is full means :Def9: :: YELLOW_6:def 9
a3 is full SubRelStr of a2;
end;

:: deftheorem Def9 defines full YELLOW_6:def 9 :
for b1 being 1-sorted
for b2 being NetStr of b1
for b3 being SubNetStr of b2 holds
( b3 is full iff b3 is full SubRelStr of b2 );

Lemma23: for b1 being 1-sorted
for b2 being NetStr of b1 holds NetStr(# the carrier of b2,the InternalRel of b2,the mapping of b2 #) is full SubRelStr of b2
proof end;

registration
let c1 be 1-sorted ;
let c2 be NetStr of c1;
cluster strict full SubNetStr of a2;
existence
ex b1 being SubNetStr of c2 st
( b1 is full & b1 is strict )
proof end;
end;

registration
let c1 be 1-sorted ;
let c2 be non empty NetStr of c1;
cluster non empty strict full SubNetStr of a2;
existence
ex b1 being SubNetStr of c2 st
( b1 is full & not b1 is empty & b1 is strict )
proof end;
end;

theorem Th19: :: YELLOW_6:19
for b1 being 1-sorted
for b2 being NetStr of b1
for b3 being SubNetStr of b2 holds the carrier of b3 c= the carrier of b2
proof end;

theorem Th20: :: YELLOW_6:20
for b1 being 1-sorted
for b2 being NetStr of b1
for b3 being SubNetStr of b2
for b4, b5 being Element of b2
for b6, b7 being Element of b3 st b4 = b6 & b5 = b7 & b6 <= b7 holds
b4 <= b5
proof end;

theorem Th21: :: YELLOW_6:21
for b1 being 1-sorted
for b2 being non empty NetStr of b1
for b3 being non empty full SubNetStr of b2
for b4, b5 being Element of b2
for b6, b7 being Element of b3 st b4 = b6 & b5 = b7 & b4 <= b5 holds
b6 <= b7
proof end;

registration
let c1 be non empty 1-sorted ;
cluster strict constant NetStr of a1;
existence
ex b1 being net of c1 st
( b1 is constant & b1 is strict )
proof end;
end;

registration
let c1 be non empty 1-sorted ;
let c2 be constant NetStr of c1;
cluster the mapping of a2 -> constant ;
coherence
the mapping of c2 is constant by Def6;
end;

definition
let c1 be non empty 1-sorted ;
let c2 be NetStr of c1;
assume E27: ( c2 is constant & not c2 is empty ) ;
func the_value_of c2 -> Element of a1 equals :Def10: :: YELLOW_6:def 10
 the_value_of the mapping of a2;
coherence
the_value_of the mapping of c2 is Element of c1
proof end;
end;

:: deftheorem Def10 defines the_value_of YELLOW_6:def 10 :
for b1 being non empty 1-sorted
for b2 being NetStr of b1 st b2 is constant & not b2 is empty holds
the_value_of b2 = the_value_of the mapping of b2;

theorem Th22: :: YELLOW_6:22
for b1 being non empty RelStr
for b2 being non empty 1-sorted
for b3 being Element of b2 holds the_value_of (b1 --> b3) = b3
proof end;

definition
let c1 be non empty 1-sorted ;
let c2 be net of c1;
canceled;
mode subnet of c2 -> net of a1 means :Def12: :: YELLOW_6:def 12
ex b1 being Function of a3,a2 st
( the mapping of a3 = the mapping of a2 * b1 & ( for b2 being Element of a2 ex b3 being Element of a3 st
for b4 being Element of a3 st b3 <= b4 holds
b2 <= b1 . b4 ) );
existence
ex b1 being net of c1ex b2 being Function of b1,c2 st
( the mapping of b1 = the mapping of c2 * b2 & ( for b3 being Element of c2 ex b4 being Element of b1 st
for b5 being Element of b1 st b4 <= b5 holds
b3 <= b2 . b5 ) )
proof end;
end;

:: deftheorem Def11 YELLOW_6:def 11 :
canceled;

:: deftheorem Def12 defines subnet YELLOW_6:def 12 :
for b1 being non empty 1-sorted
for b2, b3 being net of b1 holds
( b3 is subnet of b2 iff ex b4 being Function of b3,b2 st
( the mapping of b3 = the mapping of b2 * b4 & ( for b5 being Element of b2 ex b6 being Element of b3 st
for b7 being Element of b3 st b6 <= b7 holds
b5 <= b4 . b7 ) ) );

theorem Th23: :: YELLOW_6:23
for b1 being non empty 1-sorted
for b2 being net of b1 holds b2 is subnet of b2
proof end;

theorem Th24: :: YELLOW_6:24
for b1 being non empty 1-sorted
for b2, b3, b4 being net of b1 st b2 is subnet of b3 & b3 is subnet of b4 holds
b2 is subnet of b4
proof end;

theorem Th25: :: YELLOW_6:25
for b1 being non empty 1-sorted
for b2 being constant net of b1
for b3 being Element of b2 holds b2 . b3 = the_value_of b2
proof end;

theorem Th26: :: YELLOW_6:26
for b1 being non empty 1-sorted
for b2 being net of b1
for b3, b4 being set st b2 is_eventually_in b3 & b2 is_eventually_in b4 holds
b3 meets b4
proof end;

theorem Th27: :: YELLOW_6:27
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being subnet of b2
for b4 being set st b3 is_often_in b4 holds
b2 is_often_in b4
proof end;

theorem Th28: :: YELLOW_6:28
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being set st b2 is_eventually_in b3 holds
b2 is_often_in b3
proof end;

theorem Th29: :: YELLOW_6:29
for b1 being non empty 1-sorted
for b2 being net of b1 holds b2 is_eventually_in the carrier of b1
proof end;

definition
let c1 be 1-sorted ;
let c2 be NetStr of c1;
let c3 be set ;
func c2 " c3 -> strict SubNetStr of a2 means :Def13: :: YELLOW_6:def 13
( a4 is full SubRelStr of a2 & the carrier of a4 = the mapping of a2 " a3 );
existence
ex b1 being strict SubNetStr of c2 st
( b1 is full SubRelStr of c2 & the carrier of b1 = the mapping of c2 " c3 )
proof end;
uniqueness
for b1, b2 being strict SubNetStr of c2 st b1 is full SubRelStr of c2 & the carrier of b1 = the mapping of c2 " c3 & b2 is full SubRelStr of c2 & the carrier of b2 = the mapping of c2 " c3 holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines " YELLOW_6:def 13 :
for b1 being 1-sorted
for b2 being NetStr of b1
for b3 being set
for b4 being strict SubNetStr of b2 holds
( b4 = b2 " b3 iff ( b4 is full SubRelStr of b2 & the carrier of b4 = the mapping of b2 " b3 ) );

registration
let c1 be 1-sorted ;
let c2 be transitive NetStr of c1;
let c3 be set ;
cluster a2 " a3 -> transitive strict full ;
coherence
( c2 " c3 is transitive & c2 " c3 is full )
proof end;
end;

theorem Th30: :: YELLOW_6:30
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being set st b2 is_often_in b3 holds
( not b2 " b3 is empty & b2 " b3 is directed )
proof end;

theorem Th31: :: YELLOW_6:31
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being set st b2 is_often_in b3 holds
b2 " b3 is subnet of b2
proof end;

theorem Th32: :: YELLOW_6:32
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being set
for b4 being subnet of b2 st b4 = b2 " b3 holds
b4 is_eventually_in b3
proof end;

definition
let c1 be non empty 1-sorted ;
func NetUniv c1 -> set means :Def14: :: YELLOW_6:def 14
for b1 being set holds
( b1 in a2 iff ex b2 being strict net of a1 st
( b2 = b1 & the carrier of b2 in the_universe_of the carrier of a1 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being strict net of c1 st
( b3 = b2 & the carrier of b3 in the_universe_of the carrier of c1 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4 being strict net of c1 st
( b4 = b3 & the carrier of b4 in the_universe_of the carrier of c1 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being strict net of c1 st
( b4 = b3 & the carrier of b4 in the_universe_of the carrier of c1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines NetUniv YELLOW_6:def 14 :
for b1 being non empty 1-sorted
for b2 being set holds
( b2 = NetUniv b1 iff for b3 being set holds
( b3 in b2 iff ex b4 being strict net of b1 st
( b4 = b3 & the carrier of b4 in the_universe_of the carrier of b1 ) ) );

registration
let c1 be non empty 1-sorted ;
cluster NetUniv a1 -> non empty ;
coherence
not NetUniv c1 is empty
proof end;
end;

Lemma40: for b1, b2 being non empty 1-sorted st the carrier of b1 = the carrier of b2 holds
for b3 being constant net of b1 holds b3 is constant net of b2
proof end;

Lemma41: for b1, b2 being non empty 1-sorted st the carrier of b1 = the carrier of b2 holds
NetUniv b1 = NetUniv b2
proof end;

definition
let c1 be set ;
let c2 be 1-sorted ;
mode net_set of c1,c2 -> ManySortedSet of a1 means :Def15: :: YELLOW_6:def 15
for b1 being set st b1 in rng a3 holds
b1 is net of a2;
existence
ex b1 being ManySortedSet of c1 st
for b2 being set st b2 in rng b1 holds
b2 is net of c2
proof end;
end;

:: deftheorem Def15 defines net_set YELLOW_6:def 15 :
for b1 being set
for b2 being 1-sorted
for b3 being ManySortedSet of b1 holds
( b3 is net_set of b1,b2 iff for b4 being set st b4 in rng b3 holds
b4 is net of b2 );

theorem Th33: :: YELLOW_6:33
for b1 being set
for b2 being 1-sorted
for b3 being ManySortedSet of b1 holds
( b3 is net_set of b1,b2 iff for b4 being set st b4 in b1 holds
b3 . b4 is net of b2 )
proof end;

definition
let c1 be non empty set ;
let c2 be 1-sorted ;
let c3 be net_set of c1,c2;
let c4 be Element of c1;
redefine func . as c3 . c4 -> net of a2;
coherence
c3 . c4 is net of c2 by Th33;
end;

registration
let c1 be set ;
let c2 be 1-sorted ;
cluster -> RelStr-yielding net_set of a1,a2;
coherence
for b1 being net_set of c1,c2 holds b1 is RelStr-yielding
proof end;
end;

registration
let c1 be 1-sorted ;
let c2 be net of c1;
cluster -> RelStr-yielding yielding_non-empty_carriers net_set of the carrier of a2,a1;
coherence
for b1 being net_set of the carrier of c2,c1 holds b1 is yielding_non-empty_carriers
proof end;
end;

registration
let c1 be non empty 1-sorted ;
let c2 be net of c1;
let c3 be net_set of the carrier of c2,c1;
cluster product a3 -> non empty transitive directed ;
coherence
( product c3 is directed & product c3 is transitive )
proof end;
end;

registration
let c1 be set ;
let c2 be 1-sorted ;
cluster -> RelStr-yielding yielding_non-empty_carriers net_set of a1,a2;
coherence
for b1 being net_set of c1,c2 holds b1 is yielding_non-empty_carriers
proof end;
end;

registration
let c1 be set ;
let c2 be 1-sorted ;
cluster RelStr-yielding yielding_non-empty_carriers net_set of a1,a2;
existence
ex b1 being net_set of c1,c2 st b1 is yielding_non-empty_carriers
proof end;
end;

definition
let c1 be non empty 1-sorted ;
let c2 be net of c1;
let c3 be net_set of the carrier of c2,c1;
func Iterated c3 -> strict net of a1 means :Def16: :: YELLOW_6:def 16
( RelStr(# the carrier of a4,the InternalRel of a4 #) = [:a2,(product a3):] & ( for b1 being Element of a2
for b2 being Function st b1 in the carrier of a2 & b2 in the carrier of (product a3) holds
the mapping of a4 . b1,b2 = the mapping of (a3 . b1) . (b2 . b1) ) );
existence
ex b1 being strict net of c1 st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = [:c2,(product c3):] & ( for b2 being Element of c2
for b3 being Function st b2 in the carrier of c2 & b3 in the carrier of (product c3) holds
the mapping of b1 . b2,b3 = the mapping of (c3 . b2) . (b3 . b2) ) )
proof end;
uniqueness
for b1, b2 being strict net of c1 st RelStr(# the carrier of b1,the InternalRel of b1 #) = [:c2,(product c3):] & ( for b3 being Element of c2
for b4 being Function st b3 in the carrier of c2 & b4 in the carrier of (product c3) holds
the mapping of b1 . b3,b4 = the mapping of (c3 . b3) . (b4 . b3) ) & RelStr(# the carrier of b2,the InternalRel of b2 #) = [:c2,(product c3):] & ( for b3 being Element of c2
for b4 being Function st b3 in the carrier of c2 & b4 in the carrier of (product c3) holds
the mapping of b2 . b3,b4 = the mapping of (c3 . b3) . (b4 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines Iterated YELLOW_6:def 16 :
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being net_set of the carrier of b2,b1
for b4 being strict net of b1 holds
( b4 = Iterated b3 iff ( RelStr(# the carrier of b4,the InternalRel of b4 #) = [:b2,(product b3):] & ( for b5 being Element of b2
for b6 being Function st b5 in the carrier of b2 & b6 in the carrier of (product b3) holds
the mapping of b4 . b5,b6 = the mapping of (b3 . b5) . (b6 . b5) ) ) );

theorem Th34: :: YELLOW_6:34
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being net_set of the carrier of b2,b1 st b2 in NetUniv b1 & ( for b4 being Element of b2 holds b3 . b4 in NetUniv b1 ) holds
Iterated b3 in NetUniv b1
proof end;

theorem Th35: :: YELLOW_6:35
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being net_set of the carrier of b2,b1 holds the carrier of (Iterated b3) = [:the carrier of b2,(product (Carrier b3)):]
proof end;

theorem Th36: :: YELLOW_6:36
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being net_set of the carrier of b2,b1
for b4 being Element of b2
for b5 being Element of (product b3)
for b6 being Element of (Iterated b3) st b6 = [b4,b5] holds
(Iterated b3) . b6 = the mapping of (b3 . b4) . (b5 . b4)
proof end;

theorem Th37: :: YELLOW_6:37
for b1 being non empty 1-sorted
for b2 being net of b1
for b3 being net_set of the carrier of b2,b1 holds rng the mapping of (Iterated b3) c= union { (rng the mapping of (b3 . b4)) where B is Element of b2 : verum }
proof end;

definition
let c1 be non empty TopSpace;
let c2 be Point of c1;
func OpenNeighborhoods c2 -> RelStr equals :: YELLOW_6:def 17
(InclPoset { b1 where B is Subset of a1 : ( a2 in b1 & b1 is open ) } ) ~ ;
correctness
coherence
(InclPoset { b1 where B is Subset of c1 : ( c2 in b1 & b1 is open ) } ) ~ is RelStr ;
;
end;

:: deftheorem Def17 defines OpenNeighborhoods YELLOW_6:def 17 :
for b1 being non empty TopSpace
for b2 being Point of b1 holds OpenNeighborhoods b2 = (InclPoset { b3 where B is Subset of b1 : ( b2 in b3 & b3 is open ) } ) ~ ;

registration
let c1 be non empty TopSpace;
let c2 be Point of c1;
cluster OpenNeighborhoods a2 -> non empty ;
coherence
not OpenNeighborhoods c2 is empty
proof end;
end;

theorem Th38: :: YELLOW_6:38
for b1 being non empty TopSpace
for b2 being Point of b1
for b3 being Element of (OpenNeighborhoods b2) ex b4 being Subset of b1 st
( b4 = b3 & b2 in b4 & b4 is open )
proof end;

theorem Th39: :: YELLOW_6:39
for b1 being non empty TopSpace
for b2 being Point of b1
for b3 being Subset of b1 holds
( b3 in the carrier of (OpenNeighborhoods b2) iff ( b2 in b3 & b3 is open ) )
proof end;

theorem Th40: :: YELLOW_6:40
for b1 being non empty TopSpace
for b2 being Point of b1
for b3, b4 being Element of (OpenNeighborhoods b2) holds
( b3 <= b4 iff b4 c= b3 )
proof end;

registration
let c1 be non empty TopSpace;
let c2 be Point of c1;
cluster OpenNeighborhoods a2 -> non empty transitive directed ;
coherence
( OpenNeighborhoods c2 is transitive & OpenNeighborhoods c2 is directed )
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2 be net of c1;
defpred S1[ Point of c1] means for b1 being a_neighborhood of a1 holds c2 is_eventually_in b1;
func Lim c2 -> Subset of a1 means :Def18: :: YELLOW_6:def 18
for b1 being Point of a1 holds
( b1 in a3 iff for b2 being a_neighborhood of b1 holds a2 is_eventually_in b2 );
existence
ex b1 being Subset of c1 st
for b2 being Point of c1 holds
( b2 in b1 iff for b3 being a_neighborhood of b2 holds c2 is_eventually_in b3 )
proof end;
uniqueness
for b1, b2 being Subset of c1 st ( for b3 being Point of c1 holds
( b3 in b1 iff for b4 being a_neighborhood of b3 holds c2 is_eventually_in b4 ) ) & ( for b3 being Point of c1 holds
( b3 in b2 iff for b4 being a_neighborhood of b3 holds c2 is_eventually_in b4 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines Lim YELLOW_6:def 18 :
for b1 being non empty TopSpace
for b2 being net of b1
for b3 being Subset of b1 holds
( b3 = Lim b2 iff for b4 being Point of b1 holds
( b4 in b3 iff for b5 being a_neighborhood of b4 holds b2 is_eventually_in b5 ) );

theorem Th41: :: YELLOW_6:41
for b1 being non empty TopSpace
for b2 being net of b1
for b3 being subnet of b2 holds Lim b2 c= Lim b3
proof end;

theorem Th42: :: YELLOW_6:42
for b1 being non empty TopSpace
for b2 being constant net of b1 holds the_value_of b2 in Lim b2
proof end;

theorem Th43: :: YELLOW_6:43
for b1 being non empty TopSpace
for b2 being net of b1
for b3 being Point of b1 st b3 in Lim b2 holds
for b4 being Element of b2 ex b5 being Subset of b1 st
( b5 = { (b2 . b6) where B is Element of b2 : b4 <= b6 } & b3 in Cl b5 )
proof end;

theorem Th44: :: YELLOW_6:44
for b1 being non empty TopSpace holds
( b1 is Hausdorff iff for b2 being net of b1
for b3, b4 being Point of b1 st b3 in Lim b2 & b4 in Lim b2 holds
b3 = b4 )
proof end;

registration
let c1 be non empty Hausdorff TopSpace;
let c2 be net of c1;
cluster Lim a2 -> trivial ;
coherence
Lim c2 is trivial
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2 be net of c1;
attr a2 is convergent means :Def19: :: YELLOW_6:def 19
 Lim a2 <> {} ;
end;

:: deftheorem Def19 defines convergent YELLOW_6:def 19 :
for b1 being non empty TopSpace
for b2 being net of b1 holds
( b2 is convergent iff Lim b2 <> {} );

registration
let c1 be non empty TopSpace;
cluster constant -> convergent NetStr of a1;
coherence
for b1 being net of c1 st b1 is constant holds
b1 is convergent
proof end;
end;

registration
let c1 be non empty TopSpace;
cluster strict convergent NetStr of a1;
existence
ex b1 being net of c1 st
( b1 is convergent & b1 is strict )
proof end;
end;

definition
let c1 be non empty Hausdorff TopSpace;
let c2 be convergent net of c1;
func lim c2 -> Element of a1 means :Def20: :: YELLOW_6:def 20
a3 in Lim a2;
existence
ex b1 being Element of c1 st b1 in Lim c2
proof end;
correctness
uniqueness
for b1, b2 being Element of c1 st b1 in Lim c2 & b2 in Lim c2 holds
b1 = b2;
by REALSET1:15;
end;

:: deftheorem Def20 defines lim YELLOW_6:def 20 :
for b1 being non empty Hausdorff TopSpace
for b2 being convergent net of b1
for b3 being Element of b1 holds
( b3 = lim b2 iff b3 in Lim b2 );

theorem Th45: :: YELLOW_6:45
for b1 being non empty Hausdorff TopSpace
for b2 being constant net of b1 holds lim b2 = the_value_of b2
proof end;

theorem Th46: :: YELLOW_6:46
for b1 being non empty TopSpace
for b2 being net of b1
for b3 being Point of b1 st not b3 in Lim b2 holds
ex b4 being subnet of b2 st
for b5 being subnet of b4 holds not b3 in Lim b5
proof end;

theorem Th47: :: YELLOW_6:47
for b1 being non empty TopSpace
for b2 being net of b1 st b2 in NetUniv b1 holds
for b3 being Point of b1 st not b3 in Lim b2 holds
ex b4 being subnet of b2 st
( b4 in NetUniv b1 & ( for b5 being subnet of b4 holds not b3 in Lim b5 ) )
proof end;

theorem Th48: :: YELLOW_6:48
for b1 being non empty TopSpace
for b2 being net of b1
for b3 being Point of b1 st b3 in Lim b2 holds
for b4 being net_set of the carrier of b2,b1 st ( for b5 being Element of b2 holds b2 . b5 in Lim (b4 . b5) ) holds
b3 in Lim (Iterated b4)
proof end;

definition
let c1 be non empty 1-sorted ;
mode Convergence-Class of c1 -> set means :Def21: :: YELLOW_6:def 21
a2 c= [:(NetUniv a1),the carrier of a1:];
existence
ex b1 being set st b1 c= [:(NetUniv c1),the carrier of c1:] ;
end;

:: deftheorem Def21 defines Convergence-Class YELLOW_6:def 21 :
for b1 being non empty 1-sorted
for b2 being set holds
( b2 is Convergence-Class of b1 iff b2 c= [:(NetUniv b1),the carrier of b1:] );

registration
let c1 be non empty 1-sorted ;
cluster -> Relation-like Convergence-Class of a1;
coherence
for b1 being Convergence-Class of c1 holds b1 is Relation-like
proof end;
end;

definition
let c1 be non empty TopSpace;
func Convergence c1 -> Convergence-Class of a1 means :Def22: :: YELLOW_6:def 22
for b1 being net of a1
for b2 being Point of a1 holds
( [b1,b2] in a2 iff ( b1 in NetUniv a1 & b2 in Lim b1 ) );
existence
ex b1 being Convergence-Class of c1 st
for b2 being net of c1
for b3 being Point of c1 holds
( [b2,b3] in b1 iff ( b2 in NetUniv c1 & b3 in Lim b2 ) )
proof end;
uniqueness
for b1, b2 being Convergence-Class of c1 st ( for b3 being net of c1
for b4 being Point of c1 holds
( [b3,b4] in b1 iff ( b3 in NetUniv c1 & b4 in Lim b3 ) ) ) & ( for b3 being net of c1
for b4 being Point of c1 holds
( [b3,b4] in b2 iff ( b3 in NetUniv c1 & b4 in Lim b3 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines Convergence YELLOW_6:def 22 :
for b1 being non empty TopSpace
for b2 being Convergence-Class of b1 holds
( b2 = Convergence b1 iff for b3 being net of b1
for b4 being Point of b1 holds
( [b3,b4] in b2 iff ( b3 in NetUniv b1 & b4 in Lim b3 ) ) );

definition
let c1 be non empty 1-sorted ;
let c2 be Convergence-Class of c1;
attr a2 is (CONSTANTS) means :Def23: :: YELLOW_6:def 23
for b1 being constant net of a1 st b1 in NetUniv a1 holds
[b1,(the_value_of b1)] in a2;
attr a2 is (SUBNETS) means :Def24: :: YELLOW_6:def 24
for b1 being net of a1
for b2 being subnet of b1 st b2 in NetUniv a1 holds
for b3 being Element of a1 st [b1,b3] in a2 holds
[b2,b3] in a2;
attr a2 is (DIVERGENCE) means :Def25: :: YELLOW_6:def 25
for b1 being net of a1
for b2 being Element of a1 st b1 in NetUniv a1 & not [b1,b2] in a2 holds
ex b3 being subnet of b1 st
( b3 in NetUniv a1 & ( for b4 being subnet of b3 holds not [b4,b2] in a2 ) );
attr a2 is (ITERATED_LIMITS) means :Def26: :: YELLOW_6:def 26
for b1 being net of a1
for b2 being Element of a1 st [b1,b2] in a2 holds
for b3 being net_set of the carrier of b1,a1 st ( for b4 being Element of b1 holds [(b3 . b4),(b1 . b4)] in a2 ) holds
[(Iterated b3),b2] in a2;
end;

:: deftheorem Def23 defines (CONSTANTS) YELLOW_6:def 23 :
for b1 being non empty 1-sorted
for b2 being Convergence-Class of b1 holds
( b2 is (CONSTANTS) iff for b3 being constant net of b1 st b3 in NetUniv b1 holds
[b3,(the_value_of b3)] in b2 );

:: deftheorem Def24 defines (SUBNETS) YELLOW_6:def 24 :
for b1 being non empty 1-sorted
for b2 being Convergence-Class of b1 holds
( b2 is (SUBNETS) iff for b3 being net of b1
for b4 being subnet of b3 st b4 in NetUniv b1 holds
for b5 being Element of b1 st [b3,b5] in b2 holds
[b4,b5] in b2 );

:: deftheorem Def25 defines (DIVERGENCE) YELLOW_6:def 25 :
for b1 being non empty 1-sorted
for b2 being Convergence-Class of b1 holds
( b2 is (DIVERGENCE) iff for b3 being net of b1
for b4 being Element of b1 st b3 in NetUniv b1 & not [b3,b4] in b2 holds
ex b5 being subnet of b3 st
( b5 in NetUniv b1 & ( for b6 being subnet of b5 holds not [b6,b4] in b2 ) ) );

:: deftheorem Def26 defines (ITERATED_LIMITS) YELLOW_6:def 26 :
for b1 being non empty 1-sorted
for b2 being Convergence-Class of b1 holds
( b2 is (ITERATED_LIMITS) iff for b3 being net of b1
for b4 being Element of b1 st [b3,b4] in b2 holds
for b5 being net_set of the carrier of b3,b1 st ( for b6 being Element of b3 holds [(b5 . b6),(b3 . b6)] in b2 ) holds
[(Iterated b5),b4] in b2 );

registration
let c1 be non empty TopSpace;
cluster Convergence a1 -> Relation-like (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) ;
coherence
( Convergence c1 is (CONSTANTS) & Convergence c1 is (SUBNETS) & Convergence c1 is (DIVERGENCE) & Convergence c1 is (ITERATED_LIMITS) )
proof end;
end;

definition
let c1 be non empty 1-sorted ;
let c2 be Convergence-Class of c1;
func ConvergenceSpace c2 -> strict TopStruct means :Def27: :: YELLOW_6:def 27
( the carrier of a3 = the carrier of a1 & the topology of a3 = { b1 where B is Subset of a1 : for b1 being Element of a1 st b2 in b1 holds
for b2 being net of a1 st [b3,b2] in a2 holds
b3 is_eventually_in b1 } );
existence
ex b1 being strict TopStruct st
( the carrier of b1 = the carrier of c1 & the topology of b1 = { b2 where B is Subset of c1 : for b1 being Element of c1 st b3 in b2 holds
for b2 being net of c1 st [b4,b3] in c2 holds
b4 is_eventually_in b2 } )
proof end;
correctness
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = the carrier of c1 & the topology of b1 = { b3 where B is Subset of c1 : for b1 being Element of c1 st b4 in b3 holds
for b2 being net of c1 st [b5,b4] in c2 holds
b5 is_eventually_in b3 } & the carrier of b2 = the carrier of c1 & the topology of b2 = { b3 where B is Subset of c1 : for b1 being Element of c1 st b4 in b3 holds
for b2 being net of c1 st [b5,b4] in c2 holds
b5 is_eventually_in b3 } holds
b1 = b2;
;
end;

:: deftheorem Def27 defines ConvergenceSpace YELLOW_6:def 27 :
for b1 being non empty 1-sorted
for b2 being Convergence-Class of b1
for b3 being strict TopStruct holds
( b3 = ConvergenceSpace b2 iff ( the carrier of b3 = the carrier of b1 & the topology of b3 = { b4 where B is Subset of b1 : for b1 being Element of b1 st b5 in b4 holds
for b2 being net of b1 st [b6,b5] in b2 holds
b6 is_eventually_in b4 } ) );

registration
let c1 be non empty 1-sorted ;
let c2 be Convergence-Class of c1;
cluster ConvergenceSpace a2 -> non empty strict ;
coherence
not ConvergenceSpace c2 is empty
proof end;
end;

registration
let c1 be non empty 1-sorted ;
let c2 be Convergence-Class of c1;
cluster ConvergenceSpace a2 -> non empty strict TopSpace-like ;
coherence
ConvergenceSpace c2 is TopSpace-like
proof end;
end;

theorem Th49: :: YELLOW_6:49
for b1 being non empty 1-sorted
for b2 being Convergence-Class of b1 holds b2 c= Convergence (ConvergenceSpace b2)
proof end;

definition
let c1 be non empty 1-sorted ;
let c2 be Convergence-Class of c1;
attr a2 is topological means :Def28: :: YELLOW_6:def 28
( a2 is (CONSTANTS) & a2 is (SUBNETS) & a2 is (DIVERGENCE) & a2 is (ITERATED_LIMITS) );
end;

:: deftheorem Def28 defines topological YELLOW_6:def 28 :
for b1 being non empty 1-sorted
for b2 being Convergence-Class of b1 holds
( b2 is topological iff ( b2 is (CONSTANTS) & b2 is (SUBNETS) & b2 is (DIVERGENCE) & b2 is (ITERATED_LIMITS) ) );

registration
let c1 be non empty 1-sorted ;
cluster non empty Relation-like topological Convergence-Class of a1;
existence
ex b1 being Convergence-Class of c1 st
( not b1 is empty & b1 is topological )
proof end;
end;

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

theorem Th50: :: YELLOW_6:50
for b1 being non empty 1-sorted
for b2 being topological Convergence-Class of b1
for b3 being Subset of (ConvergenceSpace b2) holds
( b3 is open iff for b4 being Element of b1 st b4 in b3 holds
for b5 being net of b1 st [b5,b4] in b2 holds
b5 is_eventually_in b3 )
proof end;

theorem Th51: :: YELLOW_6:51
for b1 being non empty 1-sorted
for b2 being topological Convergence-Class of b1
for b3 being Subset of (ConvergenceSpace b2) holds
( b3 is closed iff for b4 being Element of b1
for b5 being net of b1 st [b5,b4] in b2 & b5 is_often_in b3 holds
b4 in b3 )
proof end;

theorem Th52: :: YELLOW_6:52
for b1 being non empty 1-sorted
for b2 being topological Convergence-Class of b1
for b3 being Subset of (ConvergenceSpace b2)
for b4 being Point of (ConvergenceSpace b2) st b4 in Cl b3 holds
ex b5 being net of ConvergenceSpace b2 st
( [b5,b4] in b2 & rng the mapping of b5 c= b3 & b4 in Lim b5 )
proof end;

theorem Th53: :: YELLOW_6:53
for b1 being non empty 1-sorted
for b2 being Convergence-Class of b1 holds
( Convergence (ConvergenceSpace b2) = b2 iff b2 is topological )
proof end;