thus SubstLatt V,C is distributive :: thesis: SubstLatt V,C is bounded

proof

let u, v, w be Element of (SubstLatt V,C); :: according to LATTICES:def 11 :: thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w)
reconsider K = u, L = v, M = w as Element of SubstitutionSet V,C by Def4;
thus u "/\" (v "\/" w) = the L_meet of (SubstLatt V,C) . K,(the L_join of (SubstLatt V,C) . L,M)
.= (u "/\" v) "\/" (u "/\" w) by Lm12 ; :: thesis: verum

end;

thus SubstLatt V,C is bounded :: thesis: verum

proof

thus SubstLatt V,C is lower-bounded :: according to LATTICES:def 15 :: thesis: SubstLatt V,C is upper-bounded

proof

set L = SubstLatt V,C;
reconsider E = {} as Element of SubstitutionSet V,C by Th1;
reconsider e = E as Element of (SubstLatt V,C) by Def4;
take e ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (SubstLatt V,C) holds
( e "/\" b₁ = e & b₁ "/\" e = e )
let u be Element of (SubstLatt V,C); :: thesis: ( e "/\" u = e & u "/\" e = e )
reconsider K = u as Element of SubstitutionSet V,C by Def4;
e "\/" u = mi (E \/ K) by Def4
.= u by Th11 ;
then ( e "/\" u = e & u "/\" e = e ) by LATTICES:def 9;
hence ( e "/\" u = e & u "/\" e = e ) ; :: thesis: verum

end;

thus SubstLatt V,C is upper-bounded :: thesis: verum

proof

set L = SubstLatt V,C;
reconsider E = {{} } as Element of SubstitutionSet V,C by Th2;
reconsider e = E as Element of (SubstLatt V,C) by Def4;
take e ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of (SubstLatt V,C) holds
( e "\/" b₁ = e & b₁ "\/" e = e )
let u be Element of (SubstLatt V,C); :: thesis: ( e "\/" u = e & u "\/" e = e )
reconsider K = u as Element of SubstitutionSet V,C by Def4;
e "/\" u = mi (E ^ K) by Def4
.= mi (K ^ E) by Th3
.= mi K by Th4
.= u by Th11 ;
then ( e "\/" u = e & u "\/" e = e ) by LATTICES:def 8;
hence ( e "\/" u = e & u "\/" e = e ) ; :: thesis: verum

end;

end;