let F be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

let F be ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) ;
let X be ( ( ) ( ) set ) ;

let F be ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) ;
let X be ( ( ) ( ) set ) ;

for X, Y, Z, D being ( ( ) ( ) set ) st D : ( ( ) ( ) set ) c= Funcs (X : ( ( ) ( ) set ) ,(Funcs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) holds
ex F being ( ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ManySortedSet of D : ( ( ) ( ) set ) ) st
( F : ( ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ManySortedSet of b₄ : ( ( ) ( ) set ) ) is uncurrying & rng F : ( ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ManySortedSet of b₄ : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) c= Funcs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) ) ;

for X, Y, Z, D being ( ( ) ( ) set ) st D : ( ( ) ( ) set ) c= Funcs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) holds
ex F being ( ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ManySortedSet of D : ( ( ) ( ) set ) ) st
( F : ( ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ManySortedSet of b₄ : ( ( ) ( ) set ) ) is currying & ( ( Y : ( ( ) ( ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) set ) implies X : ( ( ) ( ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) set ) ) implies rng F : ( ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ( Relation-like b₄ : ( ( ) ( ) set ) -defined Function-like V27(b₄ : ( ( ) ( ) set ) ) ) ManySortedSet of b₄ : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) c= Funcs (X : ( ( ) ( ) set ) ,(Funcs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) ) ) ;

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

for A, B being ( ( non empty ) ( non empty ) set )
for C being ( ( ) ( ) set )
for f, g being ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) st dom f : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) : ( ( ) ( ) set ) c= Funcs (A : ( ( non empty ) ( non empty ) set ) ,(Funcs (B : ( ( non empty ) ( non empty ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) & rng f : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) : ( ( ) ( ) set ) c= dom g : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) : ( ( ) ( ) set ) holds
g : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) * f : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = id (dom f : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) ) : ( ( ) ( ) set ) : ( ( V27( dom b₄ : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) : ( ( ) ( ) set ) ) ) ( Relation-like dom b₄ : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) : ( ( ) ( ) set ) -defined dom b₄ : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) : ( ( ) ( ) set ) -valued Function-like one-to-one V19() V21() V22() V26() V27( dom b₄ : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) : ( ( ) ( ) set ) ) quasi_total onto bijective ) Element of bool [:(dom b₄ : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) ) : ( ( ) ( ) set ) ,(dom b₄ : ( ( Relation-like Function-like commuting ) ( Relation-like Function-like commuting ) Function) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

for B being ( ( non empty ) ( non empty ) set )
for A, C being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function)
for g being ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) st dom f : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) : ( ( ) ( ) set ) c= Funcs (A : ( ( ) ( ) set ) ,(Funcs (B : ( ( non empty ) ( non empty ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) & rng f : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) : ( ( ) ( ) set ) c= dom g : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) : ( ( ) ( ) set ) holds
g : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) * f : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = id (dom f : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) ) : ( ( ) ( ) set ) : ( ( V27( dom b₄ : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) : ( ( ) ( ) set ) ) ) ( Relation-like dom b₄ : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) : ( ( ) ( ) set ) -defined dom b₄ : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) : ( ( ) ( ) set ) -valued Function-like one-to-one V19() V21() V22() V26() V27( dom b₄ : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) : ( ( ) ( ) set ) ) quasi_total onto bijective ) Element of bool [:(dom b₄ : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) ) : ( ( ) ( ) set ) ,(dom b₄ : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

for A, B, C being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function)
for g being ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) st dom f : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) : ( ( ) ( ) set ) c= Funcs ([:A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) & rng f : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) : ( ( ) ( ) set ) c= dom g : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) : ( ( ) ( ) set ) holds
g : ( ( Relation-like Function-like uncurrying ) ( Relation-like Function-like uncurrying ) Function) * f : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = id (dom f : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) ) : ( ( ) ( ) set ) : ( ( V27( dom b₄ : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) : ( ( ) ( ) set ) ) ) ( Relation-like dom b₄ : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) : ( ( ) ( ) set ) -defined dom b₄ : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) : ( ( ) ( ) set ) -valued Function-like one-to-one V19() V21() V22() V26() V27( dom b₄ : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) : ( ( ) ( ) set ) ) quasi_total onto bijective ) Element of bool [:(dom b₄ : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) ) : ( ( ) ( ) set ) ,(dom b₄ : ( ( Relation-like Function-like currying ) ( Relation-like Function-like currying ) Function) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

for f being ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) Function)
for i, A being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in dom (commute f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) set ) : ( ( ) ( ) set ) holds
((commute f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) set ) . i : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) .: A : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= pi ((f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) Function) .: A : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;

for f being ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) Function)
for i, A being ( ( ) ( ) set ) st ( for g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) Function) .: A : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
i : ( ( ) ( ) set ) in dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ) holds
pi ((f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) Function) .: A : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) c= ((commute f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) set ) . i : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) .: A : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

for X, Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= Funcs (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) holds
for i, A being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
((commute f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V33() ) set ) . i : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) .: A : ( ( ) ( ) set ) : ( ( ) ( ) set ) = pi ((f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: A : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;

for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for i, A being ( ( ) ( ) set ) st [:A : ( ( ) ( ) set ) ,{i : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) c= dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
pi (((curry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: A : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: [:A : ( ( ) ( ) set ) ,{i : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ;

let T be ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ;

let T be ( ( non empty constituted-Functions ) ( non empty constituted-Functions ) RelStr ) ;

for S, T being ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE)
for f being ( ( Function-like quasi_total idempotent ) ( non empty Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b₃ : ( ( Function-like quasi_total idempotent ) ( non empty Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full non void ) SubRelStr of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total idempotent ) ( non empty Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b₃ : ( ( Function-like quasi_total idempotent ) ( non empty Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full non void ) SubRelStr of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b₃ : ( ( Function-like quasi_total idempotent ) ( non empty Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full non void ) SubRelStr of b₂ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

for S, T, T1 being ( ( non empty ) ( non empty ) RelStr ) st T : ( ( non empty ) ( non empty ) RelStr ) is ( ( ) ( ) SubRelStr of T1 : ( ( non empty ) ( non empty ) RelStr ) ) holds
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for f1 being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f1 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
f1 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ;

for S, T, T1 being ( ( non empty ) ( non empty ) RelStr ) st T : ( ( non empty ) ( non empty ) RelStr ) is ( ( full ) ( full ) SubRelStr of T1 : ( ( non empty ) ( non empty ) RelStr ) ) holds
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for f1 being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f1 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f1 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone ;

for X being ( ( ) ( ) set )
for V being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( (chi (V : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,X : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined {{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) -valued Function-like V27(b₁ : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:b₁ : ( ( ) ( ) set ) ,{{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) " {1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = V : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & (chi (V : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,X : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined {{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) -valued Function-like V27(b₁ : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:b₁ : ( ( ) ( ) set ) ,{{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) " {0 : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) Element of K181() : ( ( ) ( ) Element of bool K177() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) set ) \ V : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

let X be ( ( non empty ) ( non empty ) set ) ;
let T be ( ( non empty ) ( non empty ) RelStr ) ;
let f be ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) ;
let x be ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func f . x -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

for X being ( ( non empty ) ( non empty ) set )
for T being ( ( non empty ) ( non empty ) RelStr )
for f, g being ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) holds
( f : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) <= g : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) iff for x being ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) holds f : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) . x : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= g : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) . x : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

for X being ( ( ) ( ) set )
for L, S being ( ( non empty ) ( non empty ) RelStr ) st RelStr(# the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of 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 Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RelStr ) = RelStr(# the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of S : ( ( 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 Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RelStr ) holds
L : ( ( non empty ) ( non empty ) RelStr ) |^ X : ( ( ) ( ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) = S : ( ( non empty ) ( non empty ) RelStr ) |^ X : ( ( ) ( ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) ;

for S1, S2, T1, T2 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st TopStruct(# the carrier of S1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) = TopStruct(# the carrier of S2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) & TopStruct(# the carrier of T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool (bool the carrier of b₃ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) = TopStruct(# the carrier of T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool (bool the carrier of b₄ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) holds
oContMaps (S1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty strict ) ( non empty strict ) RelStr ) = oContMaps (S2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty strict ) ( non empty strict ) RelStr ) ;

for X being ( ( ) ( ) set ) ex f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (BoolePoset b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of ((BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) |^ b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of (BoolePoset b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty functional ) set ) ) st
( f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (BoolePoset b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of ((BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) |^ b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of (BoolePoset b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty functional ) set ) ) is isomorphic & ( for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (BoolePoset b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of ((BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) |^ b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of (BoolePoset b₁ : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty functional ) set ) ) . Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) = chi (Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,X : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined {{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) -valued Function-like V27(b₁ : ( ( ) ( ) set ) ) quasi_total ) Element of bool [:b₁ : ( ( ) ( ) set ) ,{{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() uncurrying currying commuting ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

for X being ( ( ) ( ) set ) holds BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) ,(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean ) RelStr ) |^ X : ( ( ) ( ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) are_isomorphic ;

for X, Y being ( ( non empty ) ( non empty ) set )
for T being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset)
for S1 being ( ( non empty full ) ( non empty constituted-Functions full ) SubRelStr of (T : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ X : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ Y : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) )
for S2 being ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (T : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ Y : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ X : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) )
for F being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions full ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₂ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions full ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₂ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) st F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions full ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₂ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions full ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₂ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) is commuting holds
F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions full ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₂ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions full ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₂ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) is monotone ;

for X, Y being ( ( non empty ) ( non empty ) set )
for T being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset)
for S1 being ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (T : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ Y : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ X : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) )
for S2 being ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of T : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) )
for F being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) st F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) is uncurrying holds
F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total Function-yielding V33() ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) is monotone ;

for X, Y being ( ( non empty ) ( non empty ) set )
for T being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset)
for S1 being ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (T : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ Y : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ X : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) )
for S2 being ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of T : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) )
for F being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) st F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) is currying holds
F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -defined the carrier of b₄ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of (b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) |^ b₁ : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) -valued Function-like V27( the carrier of b₅ : ( ( non empty full ) ( non empty constituted-Functions reflexive transitive antisymmetric full non void ) SubRelStr of b₃ : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) |^ [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₂ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) ) : ( ( ) ( non empty functional ) set ) ) quasi_total ) Function of ( ( ) ( non empty functional ) set ) , ( ( ) ( non empty functional ) set ) ) is monotone ;

let S be ( ( non empty ) ( non empty ) RelStr ) ;
let T be ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) ;

let S be ( ( non empty ) ( non empty ) RelStr ) ;
let T be ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) ;

let S be ( ( non empty ) ( non empty ) RelStr ) ;
let T be ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) ;

for S being ( ( non empty ) ( non empty ) RelStr )
for T being ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) holds the carrier of (UPS (S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) )) : ( ( strict ) ( non empty constituted-Functions strict reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty functional ) set ) c= Funcs ( the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

let S be ( ( non empty ) ( non empty ) RelStr ) ;
let T be ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) ;
let f be ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) ;
let s be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
:: original: .
redefine func f . s -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

for S being ( ( non empty ) ( non empty ) RelStr )
for T being ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr )
for f, g being ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) holds
( f : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) <= g : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) iff for s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds f : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) . s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= g : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty functional ) set ) ) . s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

for S, T being ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) holds UPS (S : ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) ,T : ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric non void ) RelStr ) = SCMaps (S : ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) ,T : ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) ) : ( ( strict full ) ( non empty constituted-Functions strict reflexive transitive antisymmetric full non void ) SubRelStr of MonMaps (b₁ : ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) ,b₂ : ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) ) : ( ( strict full ) ( non empty constituted-Functions strict reflexive transitive antisymmetric full non void ) SubRelStr of b₂ : ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) |^ the carrier of b₁ : ( ( TopSpace-like reflexive transitive antisymmetric V219() V220() complete Scott ) ( non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) RelStr ) ) ) ;

for S, S9 being ( ( non empty ) ( non empty ) RelStr )
for T, T9 being ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) st RelStr(# the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of S : ( ( 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 Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RelStr ) = RelStr(# the carrier of S9 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of S9 : ( ( 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 Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RelStr ) & RelStr(# the carrier of T : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of T : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₃ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict reflexive antisymmetric non void ) RelStr ) = RelStr(# the carrier of T9 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of T9 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty Relation-like the carrier of b₄ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₄ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict reflexive antisymmetric non void ) RelStr ) holds
UPS (S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive antisymmetric non void ) RelStr ) = UPS (S9 : ( ( non empty ) ( non empty ) RelStr ) ,T9 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric non void ) RelStr ) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive antisymmetric non void ) RelStr ) ;

let S, T be ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) ;

for S, T being ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) holds UPS (S : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) ,T : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) RelStr ) is ( ( sups-inheriting ) ( non empty constituted-Functions join-inheriting sups-inheriting directed-sups-inheriting ) SubRelStr of T : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) |^ the carrier of S : ( ( reflexive transitive antisymmetric V219() V220() complete ) ( non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void ) RelStr ) ) ;