let X be ( ( empty ) ( empty ) set ) ;

for X, A being ( ( ) ( ) set ) holds (delta X : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:b₁ : ( ( ) ( ) set ) ,[:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) set ) : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= [:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ;

for X, A being ( ( ) ( ) set ) holds (delta X : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:b₁ : ( ( ) ( ) set ) ,[:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) " [:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) set ) ;

for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (delta X : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:b₁ : ( ( ) ( ) set ) ,[:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) " [:A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

for X, Y being ( ( ) ( ) set ) holds
( dom <:(pr2 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(pr1 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) & rng <:(pr2 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(pr1 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) ;

for X, Y, A, B being ( ( ) ( ) set ) holds <:(pr2 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(pr1 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: [:A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= [:B : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ;

for X, Y being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds <:(pr2 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(pr1 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: [:A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = [:B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Element of bool [:b₂ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

for X, Y being ( ( ) ( ) set ) holds <:(pr2 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(pr1 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is one-to-one ;

let X, Y be ( ( ) ( ) set ) ;

for X, Y being ( ( ) ( ) set ) holds <:(pr2 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(pr1 (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like one-to-one ) set ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = <:(pr2 (Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₂ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₂ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(pr1 (Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [:b₂ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:b₂ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like one-to-one ) set ) ;

for L1 being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice)
for L2 being ( ( non empty ) ( non empty ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for x1, y1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y1 : ( ( ) ( ) 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 non void ) Semilattice) : ( ( ) ( non empty ) set ) ) = x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

for L1 being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice)
for L2 being ( ( non empty ) ( non empty ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for x1, y1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y1 : ( ( ) ( ) 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 non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) ) = x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

for L1 being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice)
for L2 being ( ( non empty ) ( non empty ) RelStr )
for X, Y being ( ( ) ( ) Subset of )
for X1, Y1 being ( ( ) ( ) Subset of ) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & X : ( ( ) ( ) Subset of ) = X1 : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) = Y1 : ( ( ) ( ) Subset of ) holds
X : ( ( ) ( ) Subset of ) "/\" Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = X1 : ( ( ) ( ) Subset of ) "/\" Y1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

for L1 being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice)
for L2 being ( ( non empty ) ( non empty ) RelStr )
for X, Y being ( ( ) ( ) Subset of )
for X1, Y1 being ( ( ) ( ) Subset of ) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & X : ( ( ) ( ) Subset of ) = X1 : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) = Y1 : ( ( ) ( ) Subset of ) holds
X : ( ( ) ( ) Subset of ) "\/" Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = X1 : ( ( ) ( ) Subset of ) "\/" Y1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

for L1 being ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr )
for L2 being ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( waybelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = waybelow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & wayabove x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = wayabove y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

for L1 being ( ( reflexive transitive antisymmetric with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric with_infima up-complete non void satisfying_MC meet-continuous ) Semilattice)
for L2 being ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric with_infima up-complete non void satisfying_MC meet-continuous ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric with_infima up-complete non void satisfying_MC meet-continuous ) Semilattice) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric with_infima up-complete non void satisfying_MC meet-continuous ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric with_infima up-complete non void satisfying_MC meet-continuous ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric with_infima up-complete non void satisfying_MC meet-continuous ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima meet-continuous ) ( non empty reflexive transitive antisymmetric with_infima up-complete non void satisfying_MC meet-continuous ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) is meet-continuous ;

for L1 being ( ( non empty reflexive antisymmetric continuous ) ( non empty reflexive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void ) RelStr )
for L2 being ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric continuous ) ( non empty reflexive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric continuous ) ( non empty reflexive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty reflexive antisymmetric continuous ) ( non empty reflexive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive antisymmetric continuous ) ( non empty reflexive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( non empty reflexive antisymmetric continuous ) ( non empty reflexive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive antisymmetric continuous ) ( non empty reflexive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) is continuous ;

for L1, L2 being ( ( ) ( ) RelStr )
for A being ( ( ) ( ) Subset of )
for J being ( ( ) ( ) Subset of ) 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 bool [: the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) 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 bool [: the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & A : ( ( ) ( ) Subset of ) = J : ( ( ) ( ) Subset of ) holds
subrelstr A : ( ( ) ( ) Subset of ) : ( ( strict V213(b₁ : ( ( ) ( ) RelStr ) ) ) ( strict V213(b₁ : ( ( ) ( ) RelStr ) ) ) SubRelStr of b₁ : ( ( ) ( ) RelStr ) ) = subrelstr J : ( ( ) ( ) Subset of ) : ( ( strict V213(b₂ : ( ( ) ( ) RelStr ) ) ) ( strict V213(b₂ : ( ( ) ( ) RelStr ) ) ) SubRelStr of b₂ : ( ( ) ( ) RelStr ) ) ;

for L1, L2 being ( ( non empty ) ( non empty ) RelStr )
for A being ( ( ) ( ) SubRelStr of L1 : ( ( non empty ) ( non empty ) RelStr ) )
for J being ( ( ) ( ) SubRelStr of L2 : ( ( non empty ) ( non empty ) RelStr ) ) st RelStr(# the carrier of L1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & RelStr(# the carrier of A : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) , the InternalRel of A : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) -defined the carrier of b₃ : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of b₃ : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of J : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) , the InternalRel of J : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) -defined the carrier of b₄ : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₄ : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of b₄ : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & A : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) is meet-inheriting holds
J : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) is meet-inheriting ;

for L1, L2 being ( ( non empty ) ( non empty ) RelStr )
for A being ( ( ) ( ) SubRelStr of L1 : ( ( non empty ) ( non empty ) RelStr ) )
for J being ( ( ) ( ) SubRelStr of L2 : ( ( non empty ) ( non empty ) RelStr ) ) st RelStr(# the carrier of L1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & RelStr(# the carrier of A : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) , the InternalRel of A : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) -defined the carrier of b₃ : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of b₃ : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of J : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) , the InternalRel of J : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) -defined the carrier of b₄ : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₄ : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) , the carrier of b₄ : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & A : ( ( ) ( ) SubRelStr of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) is join-inheriting holds
J : ( ( ) ( ) SubRelStr of b₂ : ( ( non empty ) ( non empty ) RelStr ) ) is join-inheriting ;

for L1 being ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr )
for L2 being ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr )
for X being ( ( ) ( ) Subset of )
for Y being ( ( ) ( ) Subset of ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is property(S) holds
Y : ( ( ) ( ) Subset of ) is property(S) ;

for L1 being ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr )
for L2 being ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr )
for X being ( ( ) ( ) Subset of )
for Y being ( ( ) ( ) Subset of ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is directly_closed holds
Y : ( ( ) ( ) Subset of ) is directly_closed ;

for N being ( ( antisymmetric with_infima ) ( non empty antisymmetric with_infima ) RelStr )
for D, E being ( ( ) ( ) Subset of )
for X being ( ( upper ) ( upper ) Subset of ) st D : ( ( ) ( ) Subset of ) misses X : ( ( upper ) ( upper ) Subset of ) holds
D : ( ( ) ( ) Subset of ) "/\" E : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( antisymmetric with_infima ) ( non empty antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) misses X : ( ( upper ) ( upper ) Subset of ) ;

for R being ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) holds id the carrier of R : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued total quasi_total ) Element of bool [: the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= the InternalRel of R : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ the InternalRel of (R : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( Relation-like the carrier of (b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of (b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued the carrier of (b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of (b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) ~) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

for R being ( ( antisymmetric ) ( antisymmetric ) RelStr ) holds the InternalRel of R : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ the InternalRel of (R : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( Relation-like the carrier of (b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of (b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of (b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) -valued the carrier of (b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of (b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of (b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) ~) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= id the carrier of R : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) : ( ( total ) ( non empty Relation-like the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) -valued total quasi_total ) Element of bool [: the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

let L be ( ( non empty ) ( non empty ) RelStr ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:L : ( ( non empty ) ( non empty ) RelStr ) ,L : ( ( non empty ) ( non empty ) RelStr ) :] : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
let a, b be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
:: original: .
redefine func f . (a,b) -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

for R being ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice)
for X being ( ( ) ( ) Subset of ) st ex_inf_of (inf_op R : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total V177([:b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima non void ) RelStr ) ,b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ) ) Element of bool [: the carrier of [:b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,R : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) holds
inf_op R : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total V177([:b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima non void ) RelStr ) ,b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ) ) Element of bool [: the carrier of [:b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima upper-bounded ) ( non empty reflexive transitive antisymmetric with_infima upper-bounded non void ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) preserves_inf_of X : ( ( ) ( ) Subset of ) ;

let R be ( ( reflexive transitive antisymmetric with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V212() up-complete /\-complete non void ) Semilattice) ;

for R being ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice)
for X being ( ( ) ( ) Subset of ) st ex_sup_of (sup_op R : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total V177([:b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema non void ) RelStr ) ,b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ) ) Element of bool [: the carrier of [:b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,R : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) holds
sup_op R : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total V177([:b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema non void ) RelStr ) ,b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ) ) Element of bool [: the carrier of [:b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) ,b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded non void ) sup-Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) preserves_sup_of X : ( ( ) ( ) Subset of ) ;

let R be ( ( reflexive transitive antisymmetric with_suprema complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V212() up-complete /\-complete non void ) sup-Semilattice) ;

for N being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice)
for A being ( ( ) ( ) Subset of ) st subrelstr A : ( ( ) ( ) Subset of ) : ( ( strict V213(b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) ) ) ( strict reflexive transitive antisymmetric V213(b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) ) ) SubRelStr of b₁ : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima non void ) Semilattice) ) is meet-inheriting holds
A : ( ( ) ( ) Subset of ) is filtered ;

for N being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice)
for A being ( ( ) ( ) Subset of ) st subrelstr A : ( ( ) ( ) Subset of ) : ( ( strict V213(b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) ) ) ( strict reflexive transitive antisymmetric V213(b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) ) ) SubRelStr of b₁ : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema non void ) sup-Semilattice) ) is join-inheriting holds
A : ( ( ) ( ) Subset of ) is directed ;

for N being ( ( transitive ) ( transitive ) RelStr )
for A, J being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is_coarser_than uparrow J : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
uparrow A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= uparrow J : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

for N being ( ( transitive ) ( transitive ) RelStr )
for A, J being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is_finer_than downarrow J : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
downarrow A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= downarrow J : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

for N being ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) holds
uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered ) Element of bool the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= uparrow X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

for N being ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) holds
downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed ) Element of bool the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= downarrow X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive non void ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

for S, T being ( ( ) ( ) TopStruct )
for B being ( ( open quasi_basis ) ( open quasi_basis ) Basis of S : ( ( ) ( ) TopStruct ) ) st TopStruct(# the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) TopStruct ) = TopStruct(# the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) holds
B : ( ( open quasi_basis ) ( open quasi_basis ) Basis of b₁ : ( ( ) ( ) TopStruct ) ) is ( ( open quasi_basis ) ( open quasi_basis ) Basis of T : ( ( ) ( ) TopStruct ) ) ;

for S, T being ( ( ) ( ) TopStruct )
for B being ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of S : ( ( ) ( ) TopStruct ) ) st TopStruct(# the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) TopStruct ) = TopStruct(# the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) holds
B : ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of b₁ : ( ( ) ( ) TopStruct ) ) is ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of T : ( ( ) ( ) TopStruct ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for J being ( ( open quasi_basis ) ( open quasi_basis ) Basis of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds not J : ( ( open quasi_basis ) ( open quasi_basis ) Basis of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is empty ;

let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for J being ( ( open V225(b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ( open V225(b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) Basis of x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds not J : ( ( open V225(b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ( open V225(b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) Basis of b₂ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) is empty ;

let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let x be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

for S1, T1, S2, T2 being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st TopStruct(# the carrier of S1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of S1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of T1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) & TopStruct(# the carrier of S2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of S2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of T2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous ;