set L = PartialPredConnectivesLatt D;
thus PartialPredConnectivesLatt D is bounded ; :: according to PARTPR_1:def 17 :: thesis: ( PartialPredConnectivesLatt D is partially_complemented & PartialPredConnectivesLatt D is distributive )
thus PartialPredConnectivesLatt D is partially_complemented :: thesis: PartialPredConnectivesLatt D is distributive
proof
let b be Element of (PartialPredConnectivesLatt D); :: according to PARTPR_1:def 16 :: thesis: ex a being Element of (PartialPredConnectivesLatt D) st a is_a_partial_complement_of b
reconsider b1 = b as PartialPredicate of D by PARTFUN1:46;
reconsider a = PP_not b1 as Element of (PartialPredConnectivesLatt D) by PARTFUN1:45;
take a ; :: thesis: a is_a_partial_complement_of b
thus a is_a_partial_complement_of b by Th62; :: thesis: verum
end;
thus PartialPredConnectivesLatt D is distributive :: thesis: verum
proof
let a, b, c be Element of (PartialPredConnectivesLatt D); :: according to LATTICES:def 11 :: thesis: 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 ;
:: thesis: verum
end;