WAYBEL

:: WAYBEL_9 semantic presentation

begin

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;

cluster id L : ( ( non empty ) ( non empty ) RelStr ) : ( ( Function-like V36( the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -> Function-like V36( the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) monotone ;

end;

definition

let S, T be ( ( non empty ) ( non empty ) RelStr ) ;
let f be ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

redefine attr f is antitone means :: WAYBEL_9:def 1
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
f : ( ( ) ( Relation-like T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) -defined T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) -valued ) Element of K10(K11(T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) ,T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) >= f : ( ( ) ( Relation-like T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) -defined T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) -valued ) Element of K10(K11(T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) ,T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) . y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of T : ( ( non empty ) ( non empty ) NetStr over S : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: WAYBEL_9:1

for S, T being ( ( ) ( ) RelStr )
for K, L being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) )
for g being ( ( Function-like V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st RelStr(# the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of S : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of K : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of K : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & RelStr(# the carrier of T : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of T : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & f : ( ( Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = g : ( ( Function-like V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & f : ( ( Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is monotone holds
g : ( ( Function-like V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ;

theorem :: WAYBEL_9:2

for S, T being ( ( ) ( ) RelStr )
for K, L being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) )
for g being ( ( Function-like V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st RelStr(# the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of S : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of K : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of K : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & RelStr(# the carrier of T : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of T : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & f : ( ( Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = g : ( ( Function-like V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & f : ( ( Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is antitone holds
g : ( ( Function-like V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone ;

theorem :: WAYBEL_9:3

for A, B being ( ( ) ( ) 1-sorted )
for F being ( ( ) ( ) Subset-Family of )
for G being ( ( ) ( ) Subset-Family of ) st the carrier of A : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) = the carrier of B : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) & F : ( ( ) ( ) Subset-Family of ) = G : ( ( ) ( ) Subset-Family of ) & F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) holds
G : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) ;

theorem :: WAYBEL_9:4

errorfrm ;

theorem :: WAYBEL_9:5

errorfrm ;

theorem :: WAYBEL_9:6

for L being ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\") : ( ( Function-like V36( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) .: (uparrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered ) Element of K10( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = {y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) ;

theorem :: WAYBEL_9:7

for L being ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\") : ( ( Function-like V36( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) " {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered ) Element of K10( the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: WAYBEL_9:8

for T being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty ) ( non empty ) NetStr over T : ( ( non empty ) ( non empty ) 1-sorted ) ) holds N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) is_eventually_in rng the mapping of N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V36( the carrier of b₂ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₂ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₂ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₂ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of b₂ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

registration

let L be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
let D be ( ( non empty directed ) ( non empty directed ) Subset of ) ;
let n be ( ( Function-like V36(D : ( ( non empty directed ) ( non empty directed ) Subset of ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like D : ( ( non empty directed ) ( non empty directed ) Subset of ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(D : ( ( non empty directed ) ( non empty directed ) Subset of ) ) V36(D : ( ( non empty directed ) ( non empty directed ) Subset of ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of D : ( ( non empty directed ) ( non empty directed ) Subset of ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

cluster NetStr(# D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,( the InternalRel of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) |_2 D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( Relation-like D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued ) Element of K10(K11(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,n : ( ( Function-like V36(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) V36(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -> strict directed ;

end;

registration

let L be ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ;
let D be ( ( non empty directed ) ( non empty directed ) Subset of ) ;
let n be ( ( Function-like V36(D : ( ( non empty directed ) ( non empty directed ) Subset of ) , the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like D : ( ( non empty directed ) ( non empty directed ) Subset of ) -defined the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(D : ( ( non empty directed ) ( non empty directed ) Subset of ) ) V36(D : ( ( non empty directed ) ( non empty directed ) Subset of ) , the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of D : ( ( non empty directed ) ( non empty directed ) Subset of ) , the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

cluster NetStr(# D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,( the InternalRel of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) |_2 D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( Relation-like D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued ) Element of K10(K11(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,n : ( ( Function-like V36(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) , the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) V36(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) , the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(D : ( ( non empty directed ) ( non empty directed ) Element of K10( the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) , the carrier of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( non empty strict directed ) NetStr over L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) -> transitive strict ;

end;

theorem :: WAYBEL_9:9

for L being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) st ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) st N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) is eventually-directed holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" (sup N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) = sup ({x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of K10( the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) "/\" (rng (netmap (N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) ,L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) )) : ( ( Function-like V36( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) holds
L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) is satisfying_MC ;

theorem :: WAYBEL_9:10

for L being ( ( non empty ) ( non empty ) RelStr )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) RelStr ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( strict ) ( non empty strict directed ) NetStr over b₁ : ( ( non empty ) ( non empty ) RelStr ) ) is ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) RelStr ) ) ;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let N be ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) RelStr ) ) ;

cluster x : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) "/\" N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( strict ) ( non empty strict directed ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> transitive strict ;

end;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let N be ( ( non empty reflexive ) ( non empty reflexive ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) ;

cluster x : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) "/\" N : ( ( non empty reflexive ) ( non empty reflexive ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> reflexive strict ;

end;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let N be ( ( non empty antisymmetric ) ( non empty antisymmetric ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) ;

cluster x : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) "/\" N : ( ( non empty antisymmetric ) ( non empty antisymmetric ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> antisymmetric strict ;

end;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let N be ( ( non empty transitive ) ( non empty transitive ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) ;

cluster x : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) "/\" N : ( ( non empty transitive ) ( non empty transitive ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> transitive strict ;

end;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let J be ( ( ) ( ) set ) ;
let f be ( ( Function-like V36(J : ( ( ) ( ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like J : ( ( ) ( ) set ) -defined the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(J : ( ( ) ( ) set ) ) V36(J : ( ( ) ( ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of J : ( ( ) ( ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

cluster FinSups f : ( ( Function-like V36(J : ( ( ) ( ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like J : ( ( ) ( ) set ) -defined the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(J : ( ( ) ( ) set ) ) V36(J : ( ( ) ( ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(J : ( ( ) ( ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( non empty directed ) ( non empty directed ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> non empty transitive directed ;

end;

begin

definition

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let N be ( ( ) ( ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) ;

func inf N -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: WAYBEL_9:def 2
Inf : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

end;

definition

let L be ( ( ) ( ) RelStr ) ;
let N be ( ( ) ( ) NetStr over L : ( ( ) ( ) RelStr ) ) ;

pred ex_sup_of N means :: WAYBEL_9:def 3
ex_sup_of rng the mapping of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( Function-like V36( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) Element of K10( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,L : ( ( ) ( ) set ) ;

pred ex_inf_of N means :: WAYBEL_9:def 4
ex_inf_of rng the mapping of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( Function-like V36( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) Element of K10( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,L : ( ( ) ( ) set ) ;

end;

definition

let L be ( ( ) ( ) RelStr ) ;

func L +id -> ( ( strict ) ( strict ) NetStr over L : ( ( ) ( ) set ) ) means :: WAYBEL_9:def 5
( RelStr(# the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the InternalRel of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the InternalRel of L : ( ( ) ( ) set ) : ( ( ) ( Relation-like the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( Function-like V36( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = id L : ( ( ) ( ) set ) : ( ( Function-like V36( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V34( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V36( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) );

end;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;

cluster L : ( ( non empty ) ( non empty ) RelStr ) +id : ( ( strict ) ( strict ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> non empty strict ;

end;

registration

let L be ( ( reflexive ) ( reflexive ) RelStr ) ;

cluster L : ( ( reflexive ) ( reflexive ) RelStr ) +id : ( ( strict ) ( strict ) NetStr over L : ( ( reflexive ) ( reflexive ) RelStr ) ) -> reflexive strict ;

end;

registration

let L be ( ( antisymmetric ) ( antisymmetric ) RelStr ) ;

cluster L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) +id : ( ( strict ) ( strict ) NetStr over L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ) -> antisymmetric strict ;

end;

registration

let L be ( ( transitive ) ( transitive ) RelStr ) ;

cluster L : ( ( transitive ) ( transitive ) RelStr ) +id : ( ( strict ) ( strict ) NetStr over L : ( ( transitive ) ( transitive ) RelStr ) ) -> transitive strict ;

end;

registration

let L be ( ( with_suprema ) ( non empty with_suprema ) RelStr ) ;

cluster L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) +id : ( ( strict ) ( non empty strict ) NetStr over L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) ) -> strict directed ;

end;

registration

let L be ( ( directed ) ( directed ) RelStr ) ;

cluster L : ( ( directed ) ( directed ) RelStr ) +id : ( ( strict ) ( strict ) NetStr over L : ( ( directed ) ( directed ) RelStr ) ) -> strict directed ;

end;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;

cluster L : ( ( non empty ) ( non empty ) RelStr ) +id : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> strict monotone eventually-directed ;

end;

definition

let L be ( ( ) ( ) RelStr ) ;

func L opp+id -> ( ( strict ) ( strict ) NetStr over L : ( ( ) ( ) set ) ) means :: WAYBEL_9:def 6
( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) = the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) & the InternalRel of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = the InternalRel of L : ( ( ) ( ) set ) : ( ( ) ( Relation-like the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ~ : ( ( ) ( Relation-like the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & the mapping of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( Function-like V36( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of it : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = id L : ( ( ) ( ) set ) : ( ( Function-like V36( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V34( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V36( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) );

end;

theorem :: WAYBEL_9:11

for L being ( ( ) ( ) RelStr ) holds RelStr(# the carrier of (L : ( ( ) ( ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of (L : ( ( ) ( ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( Relation-like the carrier of (b₁ : ( ( ) ( ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of (b₁ : ( ( ) ( ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of (b₁ : ( ( ) ( ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b₁ : ( ( ) ( ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of (L : ( ( ) ( ) RelStr ) opp+id) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) set ) , the InternalRel of (L : ( ( ) ( ) RelStr ) opp+id) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( ) ( ) RelStr ) ) : ( ( ) ( Relation-like the carrier of (b₁ : ( ( ) ( ) RelStr ) opp+id) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) set ) -defined the carrier of (b₁ : ( ( ) ( ) RelStr ) opp+id) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of (b₁ : ( ( ) ( ) RelStr ) opp+id) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of (b₁ : ( ( ) ( ) RelStr ) opp+id) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( ) ( ) RelStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) ;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;

cluster L : ( ( non empty ) ( non empty ) RelStr ) opp+id : ( ( strict ) ( strict ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> non empty strict ;

end;

registration

let L be ( ( reflexive ) ( reflexive ) RelStr ) ;

cluster L : ( ( reflexive ) ( reflexive ) RelStr ) opp+id : ( ( strict ) ( strict ) NetStr over L : ( ( reflexive ) ( reflexive ) RelStr ) ) -> reflexive strict ;

end;

registration

let L be ( ( antisymmetric ) ( antisymmetric ) RelStr ) ;

cluster L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) opp+id : ( ( strict ) ( strict ) NetStr over L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ) -> antisymmetric strict ;

end;

registration

let L be ( ( transitive ) ( transitive ) RelStr ) ;

cluster L : ( ( transitive ) ( transitive ) RelStr ) opp+id : ( ( strict ) ( strict ) NetStr over L : ( ( transitive ) ( transitive ) RelStr ) ) -> transitive strict ;

end;

registration

let L be ( ( with_infima ) ( non empty with_infima ) RelStr ) ;

cluster L : ( ( with_infima ) ( non empty with_infima ) RelStr ) opp+id : ( ( strict ) ( non empty strict ) NetStr over L : ( ( with_infima ) ( non empty with_infima ) RelStr ) ) -> strict directed ;

end;

registration

let L be ( ( non empty ) ( non empty ) RelStr ) ;

cluster L : ( ( non empty ) ( non empty ) RelStr ) opp+id : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) ) -> strict antitone eventually-filtered ;

end;

definition

let L be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
let i be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

func N | i -> ( ( strict ) ( strict ) NetStr over L : ( ( ) ( ) set ) ) means :: WAYBEL_9:def 7
( ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) iff ex y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) set ) & i : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V34(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) ) V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) & the InternalRel of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( Relation-like the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -defined the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = the InternalRel of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -valued ) Element of K10(K11( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) |_2 the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -defined the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & the mapping of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( Function-like V36( the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = the mapping of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( Function-like V36( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) | the carrier of it : ( ( Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V36(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of K10(K11(N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like ) Element of K10(K11( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) );

end;

theorem :: WAYBEL_9:12

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) )
for i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds the carrier of (N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) = { y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where y is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } ;

theorem :: WAYBEL_9:13

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) )
for i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds the carrier of (N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) c= the carrier of N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL_9:14

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) )
for i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( strict ) ( strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) is ( ( full ) ( full ) SubNetStr of N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) ;

registration

let L be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty reflexive ) ( non empty reflexive ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
let i be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

cluster N : ( ( non empty reflexive ) ( non empty reflexive ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of the carrier of N : ( ( non empty reflexive ) ( non empty reflexive ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( strict ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) -> non empty reflexive strict ;

end;

registration

let L be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty directed ) ( non empty directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
let i be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

cluster N : ( ( non empty directed ) ( non empty directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of the carrier of N : ( ( non empty directed ) ( non empty directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( strict ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) -> non empty strict ;

end;

registration

let L be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
let i be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

cluster N : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of the carrier of N : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty reflexive strict ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) -> antisymmetric strict ;

end;

registration

let L be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty antisymmetric directed ) ( non empty antisymmetric directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
let i be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

cluster N : ( ( non empty antisymmetric directed ) ( non empty antisymmetric directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of the carrier of N : ( ( non empty antisymmetric directed ) ( non empty antisymmetric directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) -> antisymmetric strict ;

end;

registration

let L be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
let i be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

cluster N : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of the carrier of N : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty reflexive strict ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) -> transitive strict ;

end;

registration

cluster N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) -> transitive strict directed ;

end;

theorem :: WAYBEL_9:15

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty reflexive ) ( non empty reflexive ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) )
for i, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for x1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
N : ( ( non empty reflexive ) ( non empty reflexive ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = (N : ( ( non empty reflexive ) ( non empty reflexive ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty reflexive strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) . x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_9:16

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty directed ) ( non empty directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) )
for i, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for x1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
N : ( ( non empty directed ) ( non empty directed ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = (N : ( ( non empty directed ) ( non empty directed ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) . x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_9:17

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) )
for i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) | i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty transitive strict directed ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) is ( ( ) ( non empty transitive directed ) subnet of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) ;

registration

let T be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty transitive directed ) ( non empty transitive directed ) net of T : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

cluster non empty transitive strict directed for ( ( ) ( ) subnet of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over T : ( ( non empty ) ( non empty ) 1-sorted ) ) ) ;

end;

definition

let L be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
let i be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
:: original: |
redefine func N | i -> ( ( strict ) ( non empty transitive strict directed ) subnet of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) ) ;

end;

definition

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let T be ( ( ) ( ) 1-sorted ) ;
let f be ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) ;
let N be ( ( ) ( ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

func f * N -> ( ( strict ) ( strict ) NetStr over T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) means :: WAYBEL_9:def 8
( RelStr(# the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the InternalRel of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the InternalRel of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( Relation-like the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -valued ) Element of K10(K11( the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V36( the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) ) V36( the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of it : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = f : ( ( ) ( ) Element of the carrier of T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) * the mapping of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( Function-like V36( the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) V36( the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) -defined the carrier of T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K10(K11( the carrier of N : ( ( Function-like V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ) V36(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11(T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of T : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) );

end;

registration

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let T be ( ( ) ( ) 1-sorted ) ;
let f be ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) ;
let N be ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

cluster f : ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) * N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( strict ) ( strict ) NetStr over T : ( ( ) ( ) 1-sorted ) ) -> non empty strict ;

end;

registration

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let T be ( ( ) ( ) 1-sorted ) ;
let f be ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) ;
let N be ( ( reflexive ) ( reflexive ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

cluster f : ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) * N : ( ( reflexive ) ( reflexive ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( strict ) ( strict ) NetStr over T : ( ( ) ( ) 1-sorted ) ) -> reflexive strict ;

end;

registration

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let T be ( ( ) ( ) 1-sorted ) ;
let f be ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) ;
let N be ( ( antisymmetric ) ( antisymmetric ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

cluster f : ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) * N : ( ( antisymmetric ) ( antisymmetric ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( strict ) ( strict ) NetStr over T : ( ( ) ( ) 1-sorted ) ) -> antisymmetric strict ;

end;

registration

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let T be ( ( ) ( ) 1-sorted ) ;
let f be ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) ;
let N be ( ( transitive ) ( transitive ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

cluster f : ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) * N : ( ( transitive ) ( transitive ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( strict ) ( strict ) NetStr over T : ( ( ) ( ) 1-sorted ) ) -> transitive strict ;

end;

registration

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let T be ( ( ) ( ) 1-sorted ) ;
let f be ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) ;
let N be ( ( directed ) ( directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

cluster f : ( ( Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like V36( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of K10(K11( the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) * N : ( ( directed ) ( directed ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( strict ) ( strict ) NetStr over T : ( ( ) ( ) 1-sorted ) ) -> strict directed ;

end;

theorem :: WAYBEL_9:18

for L being ( ( non empty ) ( non empty ) RelStr )
for N being ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) RelStr ) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\") : ( ( Function-like V36( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) * N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( strict ) ( non empty strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) RelStr ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( strict ) ( non empty strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ;

begin

theorem :: WAYBEL_9:19

for S, T being ( ( ) ( ) TopStruct )
for F being ( ( ) ( ) Subset-Family of )
for G being ( ( ) ( ) Subset-Family of ) st TopStruct(# the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( open ) Element of K10(K10( the carrier of b₁ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( non empty strict ) TopStruct ) = TopStruct(# the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of T : ( ( ) ( ) TopStruct ) : ( ( ) ( open ) Element of K10(K10( the carrier of b₂ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) & F : ( ( ) ( ) Subset-Family of ) = G : ( ( ) ( ) Subset-Family of ) & F : ( ( ) ( ) Subset-Family of ) is open holds
G : ( ( ) ( ) Subset-Family of ) is open ;

theorem :: WAYBEL_9:20

for S, T being ( ( ) ( ) TopStruct )
for F being ( ( ) ( ) Subset-Family of )
for G being ( ( ) ( ) Subset-Family of ) st TopStruct(# the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( open ) Element of K10(K10( the carrier of b₁ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( non empty strict ) TopStruct ) = TopStruct(# the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of T : ( ( ) ( ) TopStruct ) : ( ( ) ( open ) Element of K10(K10( the carrier of b₂ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) & F : ( ( ) ( ) Subset-Family of ) = G : ( ( ) ( ) Subset-Family of ) & F : ( ( ) ( ) Subset-Family of ) is closed holds
G : ( ( ) ( ) Subset-Family of ) is closed ;

definition

attr c₁ is strict ;
struct TopRelStr -> ( ( ) ( ) TopStruct ) , ( ( ) ( ) RelStr ) ;
aggr TopRelStr(# carrier, InternalRel, topology #) -> ( ( strict ) ( strict ) TopRelStr ) ;

end;

registration

let A be ( ( non empty ) ( non empty ) set ) ;
let R be ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined A : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ,) ;
let T be ( ( ) ( ) Subset-Family of ) ;

cluster TopRelStr(# A : ( ( non empty ) ( non empty ) set ) ,R : ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined A : ( ( non empty ) ( non empty ) set ) -valued ) Element of K10(K11(A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,T : ( ( ) ( ) Element of K10(K10(A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) TopRelStr ) -> non empty strict ;

end;

registration

let x be ( ( ) ( ) set ) ;
let R be ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) -defined {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) -valued ) Relation of ) ;
let T be ( ( ) ( ) Subset-Family of ) ;

cluster TopRelStr(# {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) ,R : ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) -defined {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) -valued ) Element of K10(K11({x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) ,{x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,T : ( ( ) ( ) Element of K10(K10({x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( non empty strict ) TopRelStr ) -> 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element strict ;

end;

registration

let X be ( ( ) ( ) set ) ;
let O be ( ( reflexive antisymmetric transitive V34(X : ( ( ) ( ) set ) ) ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued reflexive antisymmetric transitive V34(X : ( ( ) ( ) set ) ) V36(X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) ) ) Order of X : ( ( ) ( ) set ) ) ;
let T be ( ( ) ( ) Subset-Family of ) ;

cluster TopRelStr(# X : ( ( ) ( ) set ) ,O : ( ( reflexive antisymmetric transitive V34(X : ( ( ) ( ) set ) ) ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued reflexive antisymmetric transitive V34(X : ( ( ) ( ) set ) ) V36(X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) ) ) Element of K10(K11(X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,T : ( ( ) ( ) Element of K10(K10(X : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) #) : ( ( strict ) ( strict ) TopRelStr ) -> reflexive transitive antisymmetric strict ;

end;

registration

cluster finite 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element discrete reflexive strict for ( ( ) ( ) TopRelStr ) ;

end;

definition

mode TopLattice is ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) TopRelStr ) ;

end;

registration

cluster non empty finite 1 : ( ( ) ( non empty V39() V40() V41() V45() finite cardinal ) Element of K160() : ( ( ) ( non empty V39() V40() V41() non finite cardinal limit_cardinal ) Element of K10(K156() : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element TopSpace-like Hausdorff discrete reflexive transitive antisymmetric with_suprema with_infima compact strict for ( ( ) ( ) TopRelStr ) ;

end;

registration

let T be ( ( non empty TopSpace-like Hausdorff ) ( non empty TopSpace-like T_0 T_1 Hausdorff ) TopSpace) ;

cluster non empty -> non empty Hausdorff for ( ( ) ( ) SubSpace of T : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

end;

theorem :: WAYBEL_9:21

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) a_neighborhood of p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL_9:22

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for A, B being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_9:23

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for A, B being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_9:24

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in Lim N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
for S being ( ( ) ( ) Subset of ) st S : ( ( ) ( ) Subset of ) = rng the mapping of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like V36( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in Cl S : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: WAYBEL_9:25

theorem :: WAYBEL_9:26

theorem :: WAYBEL_9:27

theorem :: WAYBEL_9:28

begin

definition

let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let N be ( ( non empty ) ( non empty ) NetStr over T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;
let p be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

pred p is_a_cluster_point_of N means :: WAYBEL_9:def 9
for O being ( ( ) ( ) a_neighborhood of p : ( ( ) ( ) Element of K10(K10(T : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over T : ( ( non empty ) ( non empty ) 1-sorted ) ) is_often_in O : ( ( ) ( ) a_neighborhood of p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;

end;

theorem :: WAYBEL_9:29

for L being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Lim N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: WAYBEL_9:30

for T being ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of T : ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace) ) ex c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace) ) ;

theorem :: WAYBEL_9:31

for L being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for M being ( ( ) ( non empty transitive directed ) subnet of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) )
for c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of M : ( ( ) ( non empty transitive directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) holds
c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: WAYBEL_9:32

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds
ex M being ( ( ) ( non empty transitive directed ) subnet of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) st x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Lim M : ( ( ) ( non empty transitive directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: WAYBEL_9:33

for L being ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace) ) st ( for c, d being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace) ) & d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace) ) holds
c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds
for s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace) ) holds
s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Lim N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace) ) : ( ( ) ( trivial ) Element of K10( the carrier of b₁ : ( ( non empty TopSpace-like Hausdorff compact ) ( non empty TopSpace-like T_0 T_1 Hausdorff compact ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: WAYBEL_9:34

for S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for A being ( ( ) ( ) Subset of ) st c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) & A : ( ( ) ( ) Subset of ) is closed & rng the mapping of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like V36( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) V36( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Element of K10(K11( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) c= A : ( ( ) ( ) Subset of ) holds
c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) ;

theorem :: WAYBEL_9:35

theorem :: WAYBEL_9:36

begin

theorem :: WAYBEL_9:37

theorem :: WAYBEL_9:38

theorem :: WAYBEL_9:39

theorem :: WAYBEL_9:40

theorem :: WAYBEL_9:41