set L = PartialPredConnectivesLatt D;
thus
PartialPredConnectivesLatt D is bounded
; PARTPR_1:def 17 ( PartialPredConnectivesLatt D is partially_complemented & PartialPredConnectivesLatt D is distributive )
thus
PartialPredConnectivesLatt D is partially_complemented
PartialPredConnectivesLatt D is distributive
thus
PartialPredConnectivesLatt D is distributive
verumproof
let a,
b,
c be
Element of
(PartialPredConnectivesLatt D);
LATTICES:def 11 a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
reconsider a1 =
a,
b1 =
b,
c1 =
c as
PartialPredicate of
D by PARTFUN1:46;
A1:
(
a "/\" b = PP_and (
a1,
b1) &
a "/\" c = PP_and (
a1,
c1) )
by Def11;
b "\/" c = PP_or (
b1,
c1)
by Def12;
hence a "/\" (b "\/" c) =
PP_and (
a1,
(PP_or (b1,c1)))
by Def11
.=
PP_or (
(PP_and (a1,b1)),
(PP_and (a1,c1)))
by Th30
.=
(a "/\" b) "\/" (a "/\" c)
by A1, Def12
;
verum
end;