WAYBEL28

:: WAYBEL28 semantic presentation

definition

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

attr f is greater_or_equal_to_id means :: WAYBEL28:def 1
for j being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= f : ( ( ) ( ) NetStr over N : ( ( ) ( ) 1-sorted ) ) . j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of N : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;

end;

theorem :: WAYBEL28:4

for N being ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) holds id N : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( Function-like V35( the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is greater_or_equal_to_id ;

theorem :: WAYBEL28:5

for N being ( ( non empty directed ) ( non empty directed ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

registration

let N be ( ( non empty directed ) ( non empty directed ) RelStr ) ;

cluster non empty Relation-like the carrier of N : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of N : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) ) V35( the carrier of N : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id for ( ( ) ( ) Element of bool [: the carrier of N : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

let N be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;

cluster non empty Relation-like the carrier of N : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of N : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) V35( the carrier of N : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id for ( ( ) ( ) Element of bool [: the carrier of N : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

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 f be ( ( Function-like V35( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty ) ( non empty ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

func N * f -> ( ( non empty strict ) ( non empty strict ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) means :: WAYBEL28:def 2
( RelStr(# the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the InternalRel of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) , the InternalRel of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( Relation-like the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like V35( the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V35( the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of it : ( ( Function-like V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) V35(N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) = the mapping of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( Function-like V35( the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) ) V35( the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) * f : ( ( ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -valued ) Element of bool [:N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ,N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) -defined the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of N : ( ( ) ( ) NetStr over L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) );

end;

theorem :: WAYBEL28:6

theorem :: WAYBEL28:7

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 f being ( ( Function-like V35( 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 ) NetStr over 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 ) NetStr over 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 ) ) V35( 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 ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) * f : ( ( Function-like V35( 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 ) NetStr over 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 ) NetStr over 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 ) ) V35( 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 ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) = NetStr(# the carrier of N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the InternalRel of N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( 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 ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: 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 ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ,( the mapping of N : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V35( 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 ) ) V35( 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 bool [: 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 ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) * f : ( ( Function-like V35( 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 ) NetStr over 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 ) NetStr over 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 ) ) V35( 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 ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( 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 ) ) V35( 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 bool [: 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 ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

theorem :: WAYBEL28:8

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr )
for f being ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( 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 transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( 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 transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) holds NetStr(# the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ,f : ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( 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 transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( 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 transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) is ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

registration

let L be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) ;
let f be ( ( Function-like V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) ) V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

cluster NetStr(# the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( Relation-like the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ,f : ( ( Function-like V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) ) V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) -> non empty transitive strict directed ;

end;

theorem :: WAYBEL28:9

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 p being ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) * p : ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty strict ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) is ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) ;

registration

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 p be ( ( Function-like V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

cluster N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) * p : ( ( Function-like V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) NetStr over L : ( ( non empty ) ( non empty ) 1-sorted ) ) -> non empty transitive strict directed ;

end;

theorem :: WAYBEL28:10

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 p being ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) in NetUniv L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) holds
N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) * p : ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty transitive strict directed ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) in NetUniv L : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL28:11

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N, M being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) st NetStr(# the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the InternalRel of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) , the mapping of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of 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 transitive directed ) ( non empty transitive directed ) net of 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 transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of 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 bool [: the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty transitive strict directed ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) = NetStr(# the carrier of M : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the InternalRel of M : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) , the mapping of M : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V35( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of 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 transitive directed ) ( non empty transitive directed ) net of 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 transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of 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 bool [: the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty transitive strict directed ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) holds
M : ( ( non empty transitive directed ) ( non empty transitive directed ) net of 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 ) ) ) ;

theorem :: WAYBEL28:12

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 p being ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) ( non empty Relation-like the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) * p : ( ( Function-like V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) ( non empty Relation-like the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( non empty 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 ) ) ) ;

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 p be ( ( Function-like V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) ( non empty Relation-like the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued Function-like V34( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) V35( the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
:: original: *
redefine func N * p -> ( ( strict ) ( non empty transitive strict directed ) subnet of N : ( ( ) ( ) set ) ) ;

end;

definition

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

func lim_inf-Convergence L -> ( ( ) ( Relation-like ) Convergence-Class of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) means :: WAYBEL28:def 3
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) st N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) RelStr ) ) in NetUniv L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) holds
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( [N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) RelStr ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff for M being ( ( ) ( non empty transitive directed ) subnet of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) RelStr ) ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = lim_inf M : ( ( ) ( non empty transitive directed ) subnet of b₁ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) RelStr ) ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) );

end;

theorem :: WAYBEL28:16

for L being ( ( non empty ) ( non empty ) RelStr )
for N being ( ( non empty transitive directed constant ) ( non empty transitive directed constant ) net of L : ( ( non empty ) ( non empty ) RelStr ) )
for M being ( ( ) ( non empty transitive directed ) subnet of N : ( ( non empty transitive directed constant ) ( non empty transitive directed constant ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ) holds
( M : ( ( ) ( non empty transitive directed ) subnet of b₂ : ( ( non empty transitive directed constant ) ( non empty transitive directed constant ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ) is constant & the_value_of N : ( ( non empty transitive directed constant ) ( non empty transitive directed constant ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) = the_value_of M : ( ( ) ( non empty transitive directed ) subnet of b₂ : ( ( non empty transitive directed constant ) ( non empty transitive directed constant ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ;

definition

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

func xi L -> ( ( ) ( ) Subset-Family of ) equals :: WAYBEL28:def 4
the topology of (ConvergenceSpace (lim_inf-Convergence L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( Relation-like ) Convergence-Class of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of (ConvergenceSpace (lim_inf-Convergence L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( Relation-like ) Convergence-Class of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

end;

theorem :: WAYBEL28:18

for L being ( ( non empty ) ( non empty ) RelStr ) holds lim_inf-Convergence L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) is (SUBNETS) ;

theorem :: WAYBEL28:20

for L being ( ( non empty ) ( non empty ) RelStr )
for N, x being ( ( ) ( ) set ) st [N : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in lim_inf-Convergence L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) holds
N : ( ( ) ( ) set ) in NetUniv L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL28:21

for L being ( ( non empty ) ( non empty ) 1-sorted )
for C1, C2 being ( ( ) ( Relation-like ) Convergence-Class of L : ( ( non empty ) ( non empty ) 1-sorted ) ) st C1 : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) c= C2 : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) holds
the topology of (ConvergenceSpace C2 : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of (ConvergenceSpace b₃ : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) c= the topology of (ConvergenceSpace C1 : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of (ConvergenceSpace b₂ : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: WAYBEL28:22

for L being ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) holds lim_inf-Convergence L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) c= Scott-Convergence L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) ;

theorem :: WAYBEL28:23

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) in the_universe_of Y : ( ( ) ( ) set ) : ( ( ) ( V9() subset-closed Tarski ) set ) ;

theorem :: WAYBEL28:24

for L being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr )
for D being ( ( non empty directed ) ( non empty directed ) Subset of ) holds Net-Str D : ( ( non empty directed ) ( non empty directed ) Subset of ) : ( ( strict ) ( non empty reflexive transitive strict directed V85(b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) eventually-directed ) NetStr over b₁ : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) ) in NetUniv L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL28:28

for L being ( ( non empty reflexive ) ( non empty reflexive ) RelStr )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) in sigma L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
A : ( ( ) ( ) Subset of ) in xi L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( ) Subset-Family of ) ;