WAYBEL

:: WAYBEL_4 semantic presentation

begin

definition

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

func L -waybelow -> ( ( ) ( Relation-like ) Relation of ) means :: WAYBEL_4:def 1
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) in it : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) );

end;

definition

let L be ( ( ) ( ) RelStr ) ;

func IntRel L -> ( ( ) ( Relation-like ) Relation of ) equals :: WAYBEL_4:def 2
the InternalRel of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

let L be ( ( ) ( ) RelStr ) ;
let R be ( ( ) ( Relation-like ) Relation of ) ;

attr R is auxiliary(i) means :: WAYBEL_4:def 3
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st [x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

attr R is auxiliary(ii) means :: WAYBEL_4:def 4
for x, y, z, u being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & [x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) & y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
[u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) ;

end;

definition

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let R be ( ( ) ( Relation-like ) Relation of ) ;

attr R is auxiliary(iii) means :: WAYBEL_4:def 5
for x, y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) in R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) & [y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) in R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) holds
[(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) in R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) ;

attr R is auxiliary(iv) means :: WAYBEL_4:def 6
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds [(Bottom L : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) in R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) ;

end;

definition

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let R be ( ( ) ( Relation-like ) Relation of ) ;

attr R is auxiliary means :: WAYBEL_4:def 7
( R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) is auxiliary(i) & R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) is auxiliary(ii) & R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) is auxiliary(iii) & R : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) is auxiliary(iv) );

end;

registration

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

cluster auxiliary -> auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) for ( ( ) ( ) Element of bool [: the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) -> auxiliary for ( ( ) ( ) Element of bool [: the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

registration

let L be ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ;

cluster Relation-like auxiliary for ( ( ) ( ) Element of bool [: the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: WAYBEL_4:1

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

cluster auxiliary(i) auxiliary(ii) -> transitive for ( ( ) ( ) Element of bool [: the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

registration

let L be ( ( ) ( ) RelStr ) ;

cluster IntRel L : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like ) Relation of ) -> auxiliary(i) ;

end;

registration

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

cluster IntRel L : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( Relation-like auxiliary(i) ) Relation of ) -> auxiliary(ii) ;

end;

registration

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

cluster IntRel L : ( ( antisymmetric with_suprema ) ( non empty antisymmetric with_suprema ) RelStr ) : ( ( ) ( Relation-like auxiliary(i) ) Relation of ) -> auxiliary(iii) ;

end;

registration

let L be ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) ;

cluster IntRel L : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) : ( ( ) ( Relation-like auxiliary(i) ) Relation of ) -> auxiliary(iv) ;

end;

definition

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

func Aux L -> ( ( ) ( ) set ) means :: WAYBEL_4:def 8
for a being ( ( ) ( ) set ) holds
( a : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) iff a : ( ( ) ( ) set ) is ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) );

end;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

cluster Aux L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( ) set ) -> non empty ;

end;

theorem :: WAYBEL_4:2

theorem :: WAYBEL_4:3

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

cluster InclPoset (Aux L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) -> strict upper-bounded ;

end;

definition

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

func AuxBottom L -> ( ( ) ( Relation-like ) Relation of ) means :: WAYBEL_4:def 9
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) in it : ( ( non empty ) ( non empty ) set ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Bottom L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( ) Element of the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) );

end;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

cluster AuxBottom L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( Relation-like ) Relation of ) -> auxiliary ;

end;

theorem :: WAYBEL_4:4

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for AR being ( ( auxiliary(iv) ) ( Relation-like auxiliary(iv) ) Relation of ) holds AuxBottom L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) c= AR : ( ( auxiliary(iv) ) ( Relation-like auxiliary(iv) ) Relation of ) ;

theorem :: WAYBEL_4:5

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

end;

theorem :: WAYBEL_4:6

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for a, b being ( ( auxiliary(i) ) ( Relation-like auxiliary(i) ) Relation of ) holds a : ( ( auxiliary(i) ) ( Relation-like auxiliary(i) ) Relation of ) /\ b : ( ( auxiliary(i) ) ( Relation-like auxiliary(i) ) Relation of ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( auxiliary(i) ) ( Relation-like auxiliary(i) ) Relation of ) ;

theorem :: WAYBEL_4:7

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for a, b being ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Relation of ) holds a : ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Relation of ) /\ b : ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Relation of ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Relation of ) ;

theorem :: WAYBEL_4:8

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for a, b being ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Relation of ) holds a : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Relation of ) /\ b : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Relation of ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Relation of ) ;

theorem :: WAYBEL_4:9

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for a, b being ( ( auxiliary(iv) ) ( Relation-like auxiliary(iv) ) Relation of ) holds a : ( ( auxiliary(iv) ) ( Relation-like auxiliary(iv) ) Relation of ) /\ b : ( ( auxiliary(iv) ) ( Relation-like auxiliary(iv) ) Relation of ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( auxiliary(iv) ) ( Relation-like auxiliary(iv) ) Relation of ) ;

theorem :: WAYBEL_4:10

theorem :: WAYBEL_4:11

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for X being ( ( non empty ) ( non empty ) Subset of ) holds meet X : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( ) set ) is ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) ;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

end;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

end;

definition

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let AR be ( ( ) ( Relation-like ) Relation of ) ;

func AR -below x -> ( ( ) ( ) Subset of ) equals :: WAYBEL_4:def 10
{ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where y is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : [y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( non empty ) ( non empty ) set ) ] : ( ( ) ( ) Element of [: the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) in AR : ( ( ) ( Relation-like ) Element of bool [:x : ( ( non empty ) ( non empty ) set ) ,x : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) } ;

func AR -above x -> ( ( ) ( ) Subset of ) equals :: WAYBEL_4:def 11
{ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where y is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : [x : ( ( non empty ) ( non empty ) set ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) in AR : ( ( ) ( Relation-like ) Element of bool [:x : ( ( non empty ) ( non empty ) set ) ,x : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) } ;

end;

theorem :: WAYBEL_4:12

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for AR being ( ( auxiliary(i) ) ( Relation-like auxiliary(i) ) Relation of ) holds AR : ( ( auxiliary(i) ) ( Relation-like auxiliary(i) ) Relation of ) -below x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) c= downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let AR be ( ( auxiliary(iv) ) ( Relation-like auxiliary(iv) ) Relation of ) ;

cluster AR : ( ( auxiliary(iv) ) ( Relation-like auxiliary(iv) ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -below x : ( ( ) ( ) Element of the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) -> non empty ;

end;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let AR be ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Relation of ) ;

cluster AR : ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -below x : ( ( ) ( ) Element of the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) -> lower ;

end;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let AR be ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Relation of ) ;

cluster AR : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -below x : ( ( ) ( ) Element of the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) -> directed ;

end;

definition

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;
let AR be ( ( auxiliary(ii) auxiliary(iii) auxiliary(iv) ) ( Relation-like auxiliary(ii) auxiliary(iii) auxiliary(iv) ) Relation of ) ;

func AR -below -> ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) means :: WAYBEL_4:def 12
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds it : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (InclPoset (Ids L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) = AR : ( ( non empty ) ( non empty ) set ) -below x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) ;

end;

theorem :: WAYBEL_4:13

for L being ( ( non empty ) ( non empty ) RelStr )
for AR being ( ( ) ( Relation-like ) Relation of )
for a being ( ( ) ( ) set )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) set ) in AR : ( ( ) ( Relation-like ) Relation of ) -below y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) iff [a : ( ( ) ( ) set ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in AR : ( ( ) ( Relation-like ) Relation of ) ) ;

theorem :: WAYBEL_4:14

for a being ( ( ) ( ) set )
for L being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice)
for AR being ( ( ) ( Relation-like ) Relation of )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) set ) in AR : ( ( ) ( Relation-like ) Relation of ) -above y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) iff [y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in AR : ( ( ) ( Relation-like ) Relation of ) ) ;

theorem :: WAYBEL_4:15

definition

let L be ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ;

func MonSet L -> ( ( strict ) ( strict ) RelStr ) means :: WAYBEL_4:def 13
for a being ( ( ) ( ) set ) holds
( ( a : ( ( ) ( ) set ) in the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) implies ex s being ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) set ) = s : ( ( ) ( ) set ) & s : ( ( ) ( ) set ) is monotone & ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds s : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of (InclPoset (Ids L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) c= downarrow x : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) & ( ex s being ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) set ) = s : ( ( ) ( ) set ) & s : ( ( ) ( ) set ) is monotone & ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds s : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of (InclPoset (Ids L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) c= downarrow x : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) implies a : ( ( ) ( ) set ) in the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) & ( for c, d being ( ( ) ( ) set ) holds
( [c : ( ( ) ( ) set ) ,d : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) iff ex f, g being ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st
( c : ( ( ) ( ) set ) = f : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & d : ( ( ) ( ) set ) = g : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) set ) in the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & d : ( ( ) ( ) set ) in the carrier of it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) <= g : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) ) ) );

end;

theorem :: WAYBEL_4:16

theorem :: WAYBEL_4:17

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for AR being ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Relation of )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
AR : ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Relation of ) -below x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( lower ) Subset of ) c= AR : ( ( auxiliary(ii) ) ( Relation-like auxiliary(ii) ) Relation of ) -below y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( lower ) Subset of ) ;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;
let AR be ( ( auxiliary(ii) auxiliary(iii) auxiliary(iv) ) ( Relation-like auxiliary(ii) auxiliary(iii) auxiliary(iv) ) Relation of ) ;

cluster AR : ( ( auxiliary(ii) auxiliary(iii) auxiliary(iv) ) ( Relation-like auxiliary(ii) auxiliary(iii) auxiliary(iv) ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -below : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total monotone ;

end;

theorem :: WAYBEL_4:18

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

cluster MonSet L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( strict ) ( strict ) RelStr ) -> non empty strict ;

end;

theorem :: WAYBEL_4:19

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) holds IdsMap L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total monotone ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the carrier of (InclPoset (Ids b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) in the carrier of (MonSet L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL_4:20

theorem :: WAYBEL_4:21

theorem :: WAYBEL_4:22

theorem :: WAYBEL_4:23

theorem :: WAYBEL_4:24

theorem :: WAYBEL_4:25

theorem :: WAYBEL_4:26

theorem :: WAYBEL_4:27

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

end;

definition

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

func Rel2Map L -> ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) means :: WAYBEL_4:def 14
for AR being ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) holds it : ( ( non empty ) ( non empty ) set ) . AR : ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) : ( ( ) ( ) set ) = AR : ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) -below : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) ;

end;

theorem :: WAYBEL_4:28

theorem :: WAYBEL_4:29

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for R1, R2 being ( ( ) ( Relation-like ) Relation of ) st R1 : ( ( ) ( Relation-like ) Relation of ) c= R2 : ( ( ) ( Relation-like ) Relation of ) holds
R1 : ( ( ) ( Relation-like ) Relation of ) -below x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) c= R2 : ( ( ) ( Relation-like ) Relation of ) -below x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) ;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

cluster Rel2Map L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total monotone ;

end;

definition

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

func Map2Rel L -> ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) means :: WAYBEL_4:def 15
for s being ( ( ) ( ) set ) st s : ( ( ) ( ) set ) in the carrier of (MonSet L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) holds
ex AR being ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) st
( AR : ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) = it : ( ( non empty ) ( non empty ) set ) . s : ( ( ) ( ) set ) : ( ( ) ( ) set ) & ( for x, y being ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in AR : ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) iff ex x9, y9 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex s9 being ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st
( x9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) set ) & y9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) set ) & s9 : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = s : ( ( ) ( ) set ) & x9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in s9 : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . y9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (InclPoset (Ids L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) ) ) ) );

end;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

cluster Map2Rel L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total monotone ;

end;

theorem :: WAYBEL_4:30

theorem :: WAYBEL_4:31

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ;

cluster Rel2Map L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like V16() quasi_total ;

end;

theorem :: WAYBEL_4:32

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) holds (Rel2Map L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) ) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like V16() total quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like one-to-one ) set ) = Map2Rel L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_4:33

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) holds Rel2Map L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded with_suprema ) sup-Semilattice) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like V16() total quasi_total monotone ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic ;

theorem :: WAYBEL_4:34

definition

let L be ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) ;
let I be ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) ) ;

func DownMap I -> ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) means :: WAYBEL_4:def 16
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= sup I : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) implies it : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (InclPoset (Ids L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) = (downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ I : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of bool the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & ( not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= sup I : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) implies it : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (InclPoset (Ids L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) = downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) );

end;

theorem :: WAYBEL_4:35

theorem :: WAYBEL_4:36

for L being ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for D being ( ( non empty lower ) ( non empty lower ) Subset of ) holds {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) "/\" D : ( ( non empty lower ) ( non empty lower ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = (downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed ) Element of bool the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ D : ( ( non empty lower ) ( non empty lower ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( reflexive antisymmetric with_infima ) ( non empty reflexive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

definition

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let AR be ( ( ) ( Relation-like ) Relation of ) ;

attr AR is approximating means :: WAYBEL_4:def 17
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup (AR : ( ( non empty ) ( non empty ) set ) -below x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

let L be ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ;
let mp be ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

attr mp is approximating means :: WAYBEL_4:def 18
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex ii being ( ( ) ( ) Subset of ) st
( ii : ( ( ) ( ) Subset of ) = mp : ( ( non empty ) ( non empty ) set ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (InclPoset (Ids L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup ii : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of L : ( ( transitive antisymmetric lower-bounded with_suprema ) ( non empty transitive antisymmetric lower-bounded with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) );

end;

theorem :: WAYBEL_4:37

for L being ( ( reflexive transitive antisymmetric lower-bounded with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete with_infima satisfying_MC meet-continuous ) Semilattice)
for I being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric lower-bounded with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete with_infima satisfying_MC meet-continuous ) Semilattice) ) holds DownMap I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete with_infima satisfying_MC meet-continuous ) Semilattice) ) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is approximating ;

theorem :: WAYBEL_4:38

registration

cluster reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous -> reflexive transitive antisymmetric lower-bounded with_suprema with_infima meet-continuous for ( ( ) ( ) RelStr ) ;

end;

theorem :: WAYBEL_4:39

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous ) LATTICE)
for I being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous ) LATTICE) ) holds DownMap I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous ) LATTICE) ) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is approximating ;

registration

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

cluster L : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) -waybelow : ( ( ) ( Relation-like ) Relation of ) -> auxiliary(i) ;

end;

registration

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

cluster L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) -waybelow : ( ( ) ( Relation-like ) Relation of ) -> auxiliary(ii) ;

end;

registration

let L be ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) ;

cluster L : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) -waybelow : ( ( ) ( Relation-like auxiliary(i) auxiliary(ii) ) Relation of ) -> auxiliary(iii) ;

end;

registration

let L be ( ( non empty reflexive transitive antisymmetric /\-complete ) ( non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima ) Poset) ;

cluster L : ( ( non empty reflexive transitive antisymmetric /\-complete ) ( non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima ) RelStr ) -waybelow : ( ( ) ( Relation-like auxiliary(i) auxiliary(ii) ) Relation of ) -> auxiliary(iii) ;

end;

registration

let L be ( ( non empty reflexive antisymmetric lower-bounded ) ( non empty reflexive antisymmetric lower-bounded ) RelStr ) ;

cluster L : ( ( non empty reflexive antisymmetric lower-bounded ) ( non empty reflexive antisymmetric lower-bounded ) RelStr ) -waybelow : ( ( ) ( Relation-like auxiliary(i) ) Relation of ) -> auxiliary(iv) ;

end;

theorem :: WAYBEL_4:40

theorem :: WAYBEL_4:41

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) holds IntRel L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( Relation-like auxiliary(i) auxiliary(ii) auxiliary(iii) ) Relation of ) is approximating ;

registration

let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous ) LATTICE) ;

cluster L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous ) RelStr ) -waybelow : ( ( ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) -> approximating ;

end;

registration

let L be ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ;

cluster Relation-like auxiliary approximating for ( ( ) ( ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

func App L -> ( ( ) ( ) set ) means :: WAYBEL_4:def 19
for a being ( ( ) ( ) set ) holds
( a : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) iff a : ( ( ) ( ) set ) is ( ( auxiliary approximating ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating ) Relation of ) );

end;

registration

cluster App L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( ) set ) -> non empty ;

end;

theorem :: WAYBEL_4:42

theorem :: WAYBEL_4:43

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds meet { ((DownMap I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (InclPoset (Ids b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) where I is ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : verum } : ( ( ) ( ) set ) = waybelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_4:44

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous ) LATTICE)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds meet { (AR : ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) -below x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Subset of ) where AR is ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) : AR : ( ( auxiliary ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) in App L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous ) LATTICE) : ( ( ) ( non empty ) set ) } : ( ( ) ( ) set ) = waybelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_4:45

theorem :: WAYBEL_4:46

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE) is continuous iff ( L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) LATTICE) is meet-continuous & ex R being ( ( auxiliary approximating ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating ) Relation of ) st
for R9 being ( ( auxiliary approximating ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating ) Relation of ) holds R : ( ( auxiliary approximating ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating ) Relation of ) c= R9 : ( ( auxiliary approximating ) ( Relation-like transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating ) Relation of ) ) ) ;

definition

let L be ( ( ) ( ) RelStr ) ;
let AR be ( ( ) ( Relation-like ) Relation of ) ;

attr AR is satisfying_SI means :: WAYBEL_4:def 20
for x, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st [x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in AR : ( ( non empty ) ( non empty ) set ) & x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
ex y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( [x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in AR : ( ( non empty ) ( non empty ) set ) & [y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in AR : ( ( non empty ) ( non empty ) set ) & x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) );

end;

definition

let L be ( ( ) ( ) RelStr ) ;
let AR be ( ( ) ( Relation-like ) Relation of ) ;

attr AR is satisfying_INT means :: WAYBEL_4:def 21
for x, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st [x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in AR : ( ( non empty ) ( non empty ) set ) holds
ex y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( [x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in AR : ( ( non empty ) ( non empty ) set ) & [y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in AR : ( ( non empty ) ( non empty ) set ) );

end;

theorem :: WAYBEL_4:47

for L being ( ( ) ( ) RelStr )
for AR being ( ( ) ( Relation-like ) Relation of ) st AR : ( ( ) ( Relation-like ) Relation of ) is satisfying_SI holds
AR : ( ( ) ( Relation-like ) Relation of ) is satisfying_INT ;

registration

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

cluster satisfying_SI -> satisfying_INT for ( ( ) ( ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: WAYBEL_4:48

theorem :: WAYBEL_4:49

theorem :: WAYBEL_4:50

theorem :: WAYBEL_4:51

registration

end;

theorem :: WAYBEL_4:52

theorem :: WAYBEL_4:53

for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous ) LATTICE)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff for D being ( ( non empty directed ) ( non empty directed ) Subset of ) st y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= sup D : ( ( non empty directed ) ( non empty directed ) Subset of ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( non empty directed ) ( non empty directed ) Subset of ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

begin

definition

let L be ( ( ) ( ) RelStr ) ;
let X be ( ( ) ( ) Subset of ) ;
let R be ( ( ) ( Relation-like ) Relation of ) ;

pred X is_directed_wrt R means :: WAYBEL_4:def 22
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in X : ( ( non empty ) ( non empty ) set ) & y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in X : ( ( non empty ) ( non empty ) set ) holds
ex z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in X : ( ( non empty ) ( non empty ) set ) & [x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & [y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) );

end;

theorem :: WAYBEL_4:54

for L being ( ( ) ( ) RelStr )
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is_directed_wrt the InternalRel of L : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
X : ( ( ) ( ) Subset of ) is directed ;

definition

let X, x be ( ( ) ( ) set ) ;
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;

pred x is_maximal_wrt X,R means :: WAYBEL_4:def 23
( x : ( ( non empty ) ( non empty ) set ) in X : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) & ( for y being ( ( ) ( ) set ) holds
( not y : ( ( ) ( ) set ) in X : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) or not y : ( ( ) ( ) set ) <> x : ( ( non empty ) ( non empty ) set ) or not [x : ( ( non empty ) ( non empty ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of X : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ) );

end;

definition

let L be ( ( ) ( ) RelStr ) ;
let X be ( ( ) ( ) set ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

pred x is_maximal_in X means :: WAYBEL_4:def 24
x : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is_maximal_wrt X : ( ( non empty ) ( non empty ) set ) , the InternalRel of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: WAYBEL_4:55

for L being ( ( ) ( ) RelStr )
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_maximal_in X : ( ( ) ( ) set ) iff ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in X : ( ( ) ( ) set ) & ( for y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( not y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in X : ( ( ) ( ) set ) or not x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) < y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ) ) ;

definition

let X, x be ( ( ) ( ) set ) ;
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;

pred x is_minimal_wrt X,R means :: WAYBEL_4:def 25
( x : ( ( non empty ) ( non empty ) set ) in X : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) & ( for y being ( ( ) ( ) set ) holds
( not y : ( ( ) ( ) set ) in X : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) or not y : ( ( ) ( ) set ) <> x : ( ( non empty ) ( non empty ) set ) or not [y : ( ( ) ( ) set ) ,x : ( ( non empty ) ( non empty ) set ) ] : ( ( ) ( ) set ) in R : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of X : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ) );

end;

definition

let L be ( ( ) ( ) RelStr ) ;
let X be ( ( ) ( ) set ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

pred x is_minimal_in X means :: WAYBEL_4:def 26
x : ( ( auxiliary(iii) ) ( Relation-like auxiliary(iii) ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is_minimal_wrt X : ( ( non empty ) ( non empty ) set ) , the InternalRel of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( Relation-like ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: WAYBEL_4:56

for L being ( ( ) ( ) RelStr )
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_minimal_in X : ( ( ) ( ) set ) iff ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in X : ( ( ) ( ) set ) & ( for y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( not y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in X : ( ( ) ( ) set ) or not x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) > y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ) ) ;

theorem :: WAYBEL_4:57

theorem :: WAYBEL_4:58

theorem :: WAYBEL_4:59

theorem :: WAYBEL_4:60

theorem :: WAYBEL_4:61

registration

cluster auxiliary approximating satisfying_INT -> auxiliary approximating satisfying_SI for ( ( ) ( ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

end;