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;

A1: SubstLatt V,C is lower-bounded

proof

reconsider E = {} as Element of SubstitutionSet V,C by Th1;
set L = SubstLatt V,C;
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;
A2: e "\/" u = mi (E \/ K) by Def4
.= u by Th11 ;
then u "/\" e = e by LATTICES:def 9;
hence ( e "/\" u = e & u "/\" e = e ) by A2, LATTICES:def 9; :: thesis: verum

end;

SubstLatt V,C is upper-bounded

proof

reconsider E = {{} } as Element of SubstitutionSet V,C by Th2;
set L = SubstLatt V,C;
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;
A3: e "/\" u = mi (E ^ K) by Def4
.= mi (K ^ E) by Th3
.= mi K by Th4
.= u by Th11 ;
then e "\/" u = e by LATTICES:def 8;
hence ( e "\/" u = e & u "\/" e = e ) by A3, LATTICES:def 8; :: thesis: verum

end;

hence SubstLatt V,C is bounded by A1; :: thesis: verum