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 Lm11 ; :: 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 b1 being Element of the carrier of (SubstLatt (V,C)) holds
( e "/\" b1 = e & b1 "/\" 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 b1 being Element of the carrier of (SubstLatt (V,C)) holds
( e "\/" b1 = e & b1 "\/" 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