YELLOW

:: YELLOW_7 semantic presentation

begin

notation

let L be ( ( ) ( ) RelStr ) ;
synonym L opp for L ~ ;

end;

for L being ( ( ) ( ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) iff ~ x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) >= ~ y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) ;

theorem :: YELLOW_7:2

for L being ( ( ) ( ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= ~ y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) >= y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) >= y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= ~ y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) >= ~ y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) >= ~ y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: YELLOW_7:3

for L being ( ( ) ( ) RelStr ) holds
( L : ( ( ) ( ) RelStr ) is empty iff L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) is empty ) ;

theorem :: YELLOW_7:4

for L being ( ( ) ( ) RelStr ) holds
( L : ( ( ) ( ) RelStr ) is reflexive iff L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) is reflexive ) ;

theorem :: YELLOW_7:5

for L being ( ( ) ( ) RelStr ) holds
( L : ( ( ) ( ) RelStr ) is antisymmetric iff L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) is antisymmetric ) ;

theorem :: YELLOW_7:6

for L being ( ( ) ( ) RelStr ) holds
( L : ( ( ) ( ) RelStr ) is transitive iff L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) is transitive ) ;

theorem :: YELLOW_7:7

errorfrm ;

registration

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

cluster L : ( ( reflexive ) ( reflexive ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) -> strict reflexive ;

end;

registration

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

cluster L : ( ( transitive ) ( transitive ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) -> strict transitive ;

end;

registration

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

cluster L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) -> strict antisymmetric ;

end;

registration

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

cluster L : ( ( non empty connected ) ( non empty connected ) RelStr ) opp : ( ( strict ) ( non empty strict ) RelStr ) -> strict connected ;

end;

theorem :: YELLOW_7:8

for L being ( ( ) ( ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for X being ( ( ) ( ) set ) holds
( ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_<=_than X : ( ( ) ( ) set ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) is_>=_than X : ( ( ) ( ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) is_>=_than X : ( ( ) ( ) set ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_<=_than X : ( ( ) ( ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_>=_than X : ( ( ) ( ) set ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) is_<=_than X : ( ( ) ( ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) is_<=_than X : ( ( ) ( ) set ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_>=_than X : ( ( ) ( ) set ) ) ) ;

theorem :: YELLOW_7:9

for L being ( ( ) ( ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for X being ( ( ) ( ) set ) holds
( ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_<=_than X : ( ( ) ( ) set ) implies ~ x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) is_>=_than X : ( ( ) ( ) set ) ) & ( ~ x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) is_>=_than X : ( ( ) ( ) set ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_<=_than X : ( ( ) ( ) set ) ) & ( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_>=_than X : ( ( ) ( ) set ) implies ~ x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) is_<=_than X : ( ( ) ( ) set ) ) & ( ~ x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) is_<=_than X : ( ( ) ( ) set ) implies x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_>=_than X : ( ( ) ( ) set ) ) ) ;

theorem :: YELLOW_7:10

for L being ( ( ) ( ) RelStr )
for X being ( ( ) ( ) set ) holds
( ex_sup_of X : ( ( ) ( ) set ) ,L : ( ( ) ( ) RelStr ) iff ex_inf_of X : ( ( ) ( ) set ) ,L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) ) ;

theorem :: YELLOW_7:11

for L being ( ( ) ( ) RelStr )
for X being ( ( ) ( ) set ) holds
( ex_sup_of X : ( ( ) ( ) set ) ,L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) iff ex_inf_of X : ( ( ) ( ) set ) ,L : ( ( ) ( ) RelStr ) ) ;

theorem :: YELLOW_7:12

for L being ( ( non empty ) ( non empty ) RelStr )
for X being ( ( ) ( ) set ) st ( ex_sup_of X : ( ( ) ( ) set ) ,L : ( ( non empty ) ( non empty ) RelStr ) or ex_inf_of X : ( ( ) ( ) set ) ,L : ( ( non empty ) ( non empty ) RelStr ) opp : ( ( strict ) ( non empty strict ) RelStr ) ) holds
"\/" (X : ( ( ) ( ) set ) ,L : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) = "/\" (X : ( ( ) ( ) set ) ,(L : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( ) set ) ) ;

theorem :: YELLOW_7:13

for L being ( ( non empty ) ( non empty ) RelStr )
for X being ( ( ) ( ) set ) st ( ex_inf_of X : ( ( ) ( ) set ) ,L : ( ( non empty ) ( non empty ) RelStr ) or ex_sup_of X : ( ( ) ( ) set ) ,L : ( ( non empty ) ( non empty ) RelStr ) opp : ( ( strict ) ( non empty strict ) RelStr ) ) holds
"/\" (X : ( ( ) ( ) set ) ,L : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) = "\/" (X : ( ( ) ( ) set ) ,(L : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( ) set ) ) ;

theorem :: YELLOW_7:14

for L1, L2 being ( ( ) ( ) RelStr ) st RelStr(# the carrier of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K32(K33( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K32(K33( the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( ) ( ) RelStr ) is with_infima holds
L2 : ( ( ) ( ) RelStr ) is with_infima ;

theorem :: YELLOW_7:15

for L1, L2 being ( ( ) ( ) RelStr ) st RelStr(# the carrier of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K32(K33( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of K32(K33( the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( ) ( ) RelStr ) is with_suprema holds
L2 : ( ( ) ( ) RelStr ) is with_suprema ;

theorem :: YELLOW_7:16

for L being ( ( ) ( ) RelStr ) holds
( L : ( ( ) ( ) RelStr ) is with_infima iff L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) is with_suprema ) ;

theorem :: YELLOW_7:17

for L being ( ( non empty ) ( non empty ) RelStr ) holds
( L : ( ( non empty ) ( non empty ) RelStr ) is complete iff L : ( ( non empty ) ( non empty ) RelStr ) opp : ( ( strict ) ( non empty strict ) RelStr ) is complete ) ;

registration

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

cluster L : ( ( with_infima ) ( non empty with_infima ) RelStr ) opp : ( ( strict ) ( non empty strict ) RelStr ) -> strict with_suprema ;

end;

registration

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

cluster L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) opp : ( ( strict ) ( non empty strict ) RelStr ) -> strict with_infima ;

end;

registration

let L be ( ( non empty complete ) ( non empty with_suprema with_infima complete lower-bounded upper-bounded bounded ) RelStr ) ;

cluster L : ( ( non empty complete ) ( non empty with_suprema with_infima complete lower-bounded upper-bounded bounded ) RelStr ) opp : ( ( strict ) ( non empty strict with_suprema with_infima ) RelStr ) -> strict complete ;

end;

theorem :: YELLOW_7:18

for L being ( ( non empty ) ( non empty ) RelStr )
for X being ( ( ) ( ) Subset of )
for Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) holds
( fininfs X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = finsups Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & finsups X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = fininfs Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: YELLOW_7:19

for L being ( ( ) ( ) RelStr )
for X being ( ( ) ( ) Subset of )
for Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) holds
( downarrow X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = uparrow Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & uparrow X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = downarrow Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of (b₁ : ( ( ) ( ) RelStr ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: YELLOW_7:20

for L being ( ( non empty ) ( non empty ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = uparrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = downarrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: YELLOW_7:21

for L being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset)
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 b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) "\/" (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW_7:22

for L being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (~ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) ) "/\" (~ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW_7:23

for L being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset)
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 b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) "/\" (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW_7:24

for L being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (~ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) ) "\/" (~ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW_7:25

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) is distributive iff L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) is distributive ) ;

registration

let L be ( ( reflexive transitive antisymmetric with_suprema with_infima distributive ) ( non empty reflexive transitive antisymmetric with_suprema with_infima distributive ) LATTICE) ;

cluster L : ( ( reflexive transitive antisymmetric with_suprema with_infima distributive ) ( non empty reflexive transitive antisymmetric with_suprema with_infima distributive ) RelStr ) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) -> strict distributive ;

end;

theorem :: YELLOW_7:26

for L being ( ( ) ( ) RelStr )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( directed ) ( directed ) Subset of ) iff x : ( ( ) ( ) set ) is ( ( filtered ) ( filtered ) Subset of ) ) ;

theorem :: YELLOW_7:27

theorem :: YELLOW_7:28

for L being ( ( ) ( ) RelStr )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( lower ) ( lower ) Subset of ) iff x : ( ( ) ( ) set ) is ( ( upper ) ( upper ) Subset of ) ) ;

theorem :: YELLOW_7:29

for L being ( ( ) ( ) RelStr )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( lower ) ( lower ) Subset of ) iff x : ( ( ) ( ) set ) is ( ( upper ) ( upper ) Subset of ) ) ;

theorem :: YELLOW_7:30

for L being ( ( ) ( ) RelStr ) holds
( L : ( ( ) ( ) RelStr ) is lower-bounded iff L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) is upper-bounded ) ;

theorem :: YELLOW_7:31

for L being ( ( ) ( ) RelStr ) holds
( L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) is lower-bounded iff L : ( ( ) ( ) RelStr ) is upper-bounded ) ;

theorem :: YELLOW_7:32

for L being ( ( ) ( ) RelStr ) holds
( L : ( ( ) ( ) RelStr ) is bounded iff L : ( ( ) ( ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) is bounded ) ;

theorem :: YELLOW_7:33

for L being ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) holds
( (Bottom L : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) = Top (L : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) & ~ (Top (L : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) = Bottom L : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: YELLOW_7:34

for L being ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) holds
( (Top L : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ~ : ( ( ) ( ) Element of the carrier of (b₁ : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) = Bottom (L : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) & ~ (Bottom (L : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) ) : ( ( ) ( ) Element of the carrier of (b₁ : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) opp) : ( ( strict ) ( non empty strict antisymmetric ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) = Top L : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: YELLOW_7:35

errorfrm ;

theorem :: YELLOW_7:36

errorfrm ;

registration

let L be ( ( lower-bounded ) ( lower-bounded ) RelStr ) ;

cluster L : ( ( lower-bounded ) ( lower-bounded ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) -> strict upper-bounded ;

end;

registration

let L be ( ( upper-bounded ) ( upper-bounded ) RelStr ) ;

cluster L : ( ( upper-bounded ) ( upper-bounded ) RelStr ) opp : ( ( strict ) ( strict ) RelStr ) -> strict lower-bounded ;

end;

registration end;

theorem :: YELLOW_7:37

definition

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

func ComplMap L -> ( ( Function-like V18( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of (L : ( ( ) ( ) set ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of (L : ( ( ) ( ) set ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of (L : ( ( ) ( ) set ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) means :: YELLOW_7:def 1
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds it : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (L : ( ( ) ( ) set ) opp) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) = 'not' x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

let L be ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded bounded distributive V222() complemented Boolean ) LATTICE) ;

end;

registration

end;

theorem :: YELLOW_7:38

theorem :: YELLOW_7:39

for S, T being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( ) ( ) set ) holds
( ( f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) implies f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) & ( f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) implies f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) & ( f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) implies f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) & ( f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) implies f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) & ( f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) implies f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) & ( f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) implies f : ( ( ) ( ) set ) is ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: YELLOW_7:40

for S, T being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = g : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( ( f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone implies g : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone ) & ( g : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone implies f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ) & ( f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone implies g : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ) & ( g : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone implies f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone ) ) ;

theorem :: YELLOW_7:41

for S, T being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( ( f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone implies g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ) & ( g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone implies f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ) & ( f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone implies g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone ) & ( g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone implies f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone ) ) ;

theorem :: YELLOW_7:42

for S, T being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( ( f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone implies g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ) & ( g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone implies f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ) & ( f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone implies g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone ) & ( g : ( ( Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (b₁ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₂ : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone implies f : ( ( Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is antitone ) ) ;

theorem :: YELLOW_7:43

for S, T being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( ) ( ) set ) holds
( ( f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ) implies f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ~ : ( ( strict ) ( non empty strict ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ) ) & ( f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ~ : ( ( strict ) ( non empty strict ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ) implies f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ) ) & ( f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ) implies f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ~ : ( ( strict ) ( non empty strict ) RelStr ) ) ) & ( f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ~ : ( ( strict ) ( non empty strict ) RelStr ) ) implies f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ) ) & ( f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ) implies f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ~ : ( ( strict ) ( non empty strict ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ~ : ( ( strict ) ( non empty strict ) RelStr ) ) ) & ( f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ~ : ( ( strict ) ( non empty strict ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ~ : ( ( strict ) ( non empty strict ) RelStr ) ) implies f : ( ( ) ( ) set ) is ( ( ) ( ) Connection of S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) ) ) ) ;

theorem :: YELLOW_7:44

theorem :: YELLOW_7:45

for J being ( ( ) ( ) set )
for D being ( ( non empty ) ( non empty ) set )
for K being ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) ) ManySortedSet of J : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) Function-yielding V105() ) DoubleIndexedSet of K : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ,J : ( ( ) ( ) set ) ) holds doms F : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) Function-yielding V105() ) DoubleIndexedSet of b₃ : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ,b₁ : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = K : ( ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined Function-like V17(b₁ : ( ( ) ( ) set ) ) ) ManySortedSet of b₁ : ( ( ) ( ) set ) ) ;

definition

let J, D be ( ( non empty ) ( non empty ) set ) ;
let K be ( ( Relation-like V8() J : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(J : ( ( non empty ) ( non empty ) set ) ) ) ( non empty Relation-like V8() non empty-yielding J : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(J : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of J : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( non empty Relation-like non-empty non empty-yielding J : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(J : ( ( non empty ) ( non empty ) set ) ) Function-yielding V105() ) DoubleIndexedSet of K : ( ( Relation-like V8() J : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(J : ( ( non empty ) ( non empty ) set ) ) ) ( non empty Relation-like V8() non empty-yielding J : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(J : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of J : ( ( non empty ) ( non empty ) set ) ) ,J : ( ( non empty ) ( non empty ) set ) ) ;
let j be ( ( ) ( ) Element of J : ( ( non empty ) ( non empty ) set ) ) ;
let k be ( ( ) ( ) Element of K : ( ( Relation-like V8() J : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(J : ( ( non empty ) ( non empty ) set ) ) ) ( non empty Relation-like V8() non empty-yielding J : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(J : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of J : ( ( non empty ) ( non empty ) set ) ) . j : ( ( ) ( ) Element of J : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
:: original: ..
redefine func F .. (j,k) -> ( ( ) ( ) Element of D : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ;

end;

theorem :: YELLOW_7:46

for L being ( ( non empty ) ( non empty ) RelStr )
for J being ( ( ) ( ) set )
for K being ( ( Relation-like b₂ : ( ( ) ( ) set ) -defined Function-like V17(b₂ : ( ( ) ( ) set ) ) ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined Function-like V17(b₂ : ( ( ) ( ) set ) ) ) ManySortedSet of J : ( ( ) ( ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined Function-like V17(b₂ : ( ( ) ( ) set ) ) Function-yielding V105() ) DoubleIndexedSet of K : ( ( Relation-like b₂ : ( ( ) ( ) set ) -defined Function-like V17(b₂ : ( ( ) ( ) set ) ) ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined Function-like V17(b₂ : ( ( ) ( ) set ) ) ) ManySortedSet of b₂ : ( ( ) ( ) set ) ) ,) iff x : ( ( ) ( ) set ) is ( ( ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined Function-like V17(b₂ : ( ( ) ( ) set ) ) Function-yielding V105() ) DoubleIndexedSet of K : ( ( Relation-like b₂ : ( ( ) ( ) set ) -defined Function-like V17(b₂ : ( ( ) ( ) set ) ) ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined Function-like V17(b₂ : ( ( ) ( ) set ) ) ) ManySortedSet of b₂ : ( ( ) ( ) set ) ) ,) ) ;

theorem :: YELLOW_7:47

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete ) LATTICE)
for J being ( ( non empty ) ( non empty ) set )
for K being ( ( Relation-like V8() b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(b₂ : ( ( non empty ) ( non empty ) set ) ) ) ( non empty Relation-like V8() non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(b₂ : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of J : ( ( non empty ) ( non empty ) set ) )
for F being ( ( ) ( non empty Relation-like non-empty non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(b₂ : ( ( non empty ) ( non empty ) set ) ) Function-yielding V105() ) DoubleIndexedSet of K : ( ( Relation-like V8() b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(b₂ : ( ( non empty ) ( non empty ) set ) ) ) ( non empty Relation-like V8() non empty-yielding b₂ : ( ( non empty ) ( non empty ) set ) -defined Function-like V17(b₂ : ( ( non empty ) ( non empty ) set ) ) ) ManySortedSet of b₂ : ( ( non empty ) ( non empty ) set ) ) ,) holds Sup : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete ) LATTICE) : ( ( ) ( non empty ) set ) ) <= Inf : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded up-complete /\-complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW_7:48

theorem :: YELLOW_7:49

theorem :: YELLOW_7:50

registration

cluster non empty completely-distributive -> non empty complete for ( ( ) ( ) RelStr ) ;

end;

registration

cluster non empty V45() finite 1 : ( ( ) ( non empty V24() V25() V26() V30() finite V36() countable ) Element of K229() : ( ( ) ( non empty V5() V24() V25() V26() non finite V36() V37() countable denumerable ) Element of K32(K225() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) -element strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded connected up-complete /\-complete distributive V222() completely-distributive for ( ( ) ( ) RelStr ) ;

end;

theorem :: YELLOW_7:51

for L being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) holds
( L : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) is completely-distributive iff L : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is completely-distributive ) ;