:: SUBSTLAT semantic presentation

begin

definition
let V, C be ( ( ) ( ) set ) ;
func SubstitutionSet (V,C) -> ( ( ) ( ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) equals :: SUBSTLAT:def 1
 { A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) where A is ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) LattStr ) ,C : ( ( Function-like V18(K20(V : ( ( ) ( ) LattStr ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) LattStr ) ) ) ( V1() V4(K20(V : ( ( ) ( ) LattStr ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) LattStr ) ) Function-like V18(K20(V : ( ( ) ( ) LattStr ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) LattStr ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( for u being ( ( ) ( ) set ) st u : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
u : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) is finite ) & ( for s, t being ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) LattStr ) ,C : ( ( Function-like V18(K20(V : ( ( ) ( ) LattStr ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) LattStr ) ) ) ( V1() V4(K20(V : ( ( ) ( ) LattStr ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) LattStr ) ) Function-like V18(K20(V : ( ( ) ( ) LattStr ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) LattStr ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) st s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) c= t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) holds
s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) = t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) ) } ;
end;

theorem :: SUBSTLAT:1
for V, C being ( ( ) ( ) set ) holds {} : ( ( ) ( Function-like functional empty finite V39() ) set ) in SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:2
for V, C being ( ( ) ( ) set ) holds {{} : ( ( ) ( Function-like functional empty finite V39() ) set ) } : ( ( ) ( non empty finite V39() ) set ) in SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ;

registration
let V, C be ( ( ) ( ) set ) ;
cluster SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) -> non empty ;
end;

definition
let V, C be ( ( ) ( ) set ) ;
let A, B be ( ( ) ( ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;
:: original: \/
redefine func A \/ B -> ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( V1() Function-like ) ( V1() Function-like ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;
end;

registration
let V, C be ( ( ) ( ) set ) ;
cluster non empty for ( ( ) ( ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;
end;

registration
let V, C be ( ( ) ( ) set ) ;
cluster -> finite for ( ( ) ( ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;
end;

definition
let V, C be ( ( ) ( ) set ) ;
let A be ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;
func mi A -> ( ( ) ( finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) equals :: SUBSTLAT:def 2
 { t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) where t is ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) : ( t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) is finite & ( for s being ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) holds
( ( s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) & s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) c= t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) iff s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) = t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) ) ) } ;
end;

registration
let V, C be ( ( ) ( ) set ) ;
cluster -> functional for ( ( ) ( ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;
end;

definition
let V, C be ( ( ) ( ) set ) ;
let A, B be ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;
func A ^ B -> ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) equals :: SUBSTLAT:def 3
 { (s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) \/ t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( ) set ) where s, t is ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) : ( s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) & t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) in B : ( ( Function-like ) ( V1() V4(V : ( ( ) ( ) set ) ) V5(C : ( ( ) ( ) set ) ) Function-like ) Element of K19(K20(V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) & s : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) tolerates t : ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) } ;
end;

theorem :: SUBSTLAT:3
for V, C being ( ( ) ( ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:4
for V, C being ( ( ) ( ) set )
for B, A being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) st B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = {{} : ( ( ) ( Function-like functional empty finite V39() ) set ) } : ( ( ) ( non empty finite V39() ) set ) holds
A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:5
for V, C being ( ( ) ( ) set )
for B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) )
for a, b being ( ( ) ( ) set ) st B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) in SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) & a : ( ( ) ( ) set ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & b : ( ( ) ( ) set ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & a : ( ( ) ( ) set ) c= b : ( ( ) ( ) set ) holds
a : ( ( ) ( ) set ) = b : ( ( ) ( ) set ) ;

theorem :: SUBSTLAT:6
for V, C being ( ( ) ( ) set )
for B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) )
for a being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in mi B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) holds
( a : ( ( ) ( ) set ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & ( for b being ( ( ) ( ) set ) st b : ( ( ) ( ) set ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & b : ( ( ) ( ) set ) c= a : ( ( ) ( ) set ) holds
b : ( ( ) ( ) set ) = a : ( ( ) ( ) set ) ) ) ;

registration
let V, C be ( ( ) ( ) set ) ;
cluster V1() Function-like finite for ( ( ) ( ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) ;
end;

theorem :: SUBSTLAT:7
for V, C being ( ( ) ( ) set )
for B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) )
for a being ( ( finite ) ( finite ) set ) st a : ( ( finite ) ( finite ) set ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & ( for b being ( ( finite ) ( finite ) set ) st b : ( ( finite ) ( finite ) set ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & b : ( ( finite ) ( finite ) set ) c= a : ( ( finite ) ( finite ) set ) holds
b : ( ( finite ) ( finite ) set ) = a : ( ( finite ) ( finite ) set ) ) holds
a : ( ( finite ) ( finite ) set ) in mi B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;

theorem :: SUBSTLAT:8
for V, C being ( ( ) ( ) set )
for A being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds mi A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) c= A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:9
for V, C being ( ( ) ( ) set )
for A being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) st A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = {} : ( ( ) ( Function-like functional empty finite V39() ) set ) holds
mi A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) = {} : ( ( ) ( Function-like functional empty finite V39() ) set ) ;

theorem :: SUBSTLAT:10
for V, C being ( ( ) ( ) set )
for B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) )
for b being ( ( finite ) ( finite ) set ) st b : ( ( finite ) ( finite ) set ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
ex c being ( ( ) ( ) set ) st
( c : ( ( ) ( ) set ) c= b : ( ( finite ) ( finite ) set ) & c : ( ( ) ( ) set ) in mi B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ) ;

theorem :: SUBSTLAT:11
for V, C being ( ( ) ( ) set )
for K being ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) holds mi K : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) = K : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;

theorem :: SUBSTLAT:12
for V, C being ( ( ) ( ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds mi (A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) \/ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) c= (mi A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) \/ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:13
for V, C being ( ( ) ( ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds mi ((mi A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) \/ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) = mi (A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) \/ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;

theorem :: SUBSTLAT:14
for V, C being ( ( ) ( ) set )
for A, B, D being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) st A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) c= B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ D : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) c= B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ D : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:15
for V, C being ( ( ) ( ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) )
for a being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
ex b, c being ( ( ) ( ) set ) st
( b : ( ( ) ( ) set ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & c : ( ( ) ( ) set ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & a : ( ( ) ( ) set ) = b : ( ( ) ( ) set ) \/ c : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: SUBSTLAT:16
for V, C being ( ( ) ( ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) )
for b, c being ( ( ) ( V1() Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) st b : ( ( ) ( V1() Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & c : ( ( ) ( V1() Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) in B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & b : ( ( ) ( V1() Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) tolerates c : ( ( ) ( V1() Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) holds
b : ( ( ) ( V1() Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) \/ c : ( ( ) ( V1() Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) : ( ( ) ( ) set ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:17
for V, C being ( ( ) ( ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds mi (A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) c= (mi A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:18
for V, C being ( ( ) ( ) set )
for A, B, D being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) st A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) c= B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
D : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) c= D : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:19
for V, C being ( ( ) ( ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds mi ((mi A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) = mi (A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;

theorem :: SUBSTLAT:20
for V, C being ( ( ) ( ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds mi (A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ (mi B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) = mi (A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;

theorem :: SUBSTLAT:21
for V, C being ( ( ) ( ) set )
for K, L, M being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds K : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ (L : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ M : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = (K : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ L : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ M : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:22
for V, C being ( ( ) ( ) set )
for K, L, M being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds K : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ (L : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) \/ M : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = (K : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ L : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) \/ (K : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ M : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:23
for V, C being ( ( ) ( ) set )
for B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) c= B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: SUBSTLAT:24
for V, C being ( ( ) ( ) set )
for A being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds mi (A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ^ A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) = mi A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;

theorem :: SUBSTLAT:25
for V, C being ( ( ) ( ) set )
for K being ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) holds mi (K : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ^ K : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) = K : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ;

begin

definition
let V, C be ( ( ) ( ) set ) ;
func SubstLatt (V,C) -> ( ( strict ) ( strict ) LattStr ) means :: SUBSTLAT:def 4
( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) = SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) & ( for A, B being ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) holds
( the L_join of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( Function-like V18(K20( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) ) ( V1() V4(K20( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) Function-like V18(K20( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20(K20( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) . (A : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ,B : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) set ) = mi (A : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) \/ B : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) & the L_meet of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( Function-like V18(K20( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) ) ( V1() V4(K20( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) Function-like V18(K20( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20(K20( the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) ( V1() V4(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like V18(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) ) Element of K19(K20(K20(V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) . (A : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ,B : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) set ) = mi (A : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ^ B : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( cup-closed diff-closed preBoolean ) set ) ) ) ) ) );
end;

registration
let V, C be ( ( ) ( ) set ) ;
cluster SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) LattStr ) -> non empty strict ;
end;

registration
let V, C be ( ( ) ( ) set ) ;
cluster SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict ) LattStr ) -> strict Lattice-like ;
end;

registration
let V, C be ( ( ) ( ) set ) ;
cluster SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -> strict distributive bounded ;
end;

theorem :: SUBSTLAT:26
for V, C being ( ( ) ( ) set ) holds Bottom (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded ) LattStr ) : ( ( ) ( ) Element of the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded ) LattStr ) : ( ( ) ( ) set ) ) = {} : ( ( ) ( Function-like functional empty finite V39() ) set ) ;

theorem :: SUBSTLAT:27
for V, C being ( ( ) ( ) set ) holds Top (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded ) LattStr ) : ( ( ) ( ) Element of the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded ) LattStr ) : ( ( ) ( ) set ) ) = {{} : ( ( ) ( Function-like functional empty finite V39() ) set ) } : ( ( ) ( non empty finite V39() ) set ) ;