let D be non empty set ; :: thesis: for p, q, r being PartialPredicate of D holds PP_or (p,(PP_and (q,r))) = PP_and ((PP_or (p,q)),(PP_or (p,r)))
let p, q, r be PartialPredicate of D; :: thesis: PP_or (p,(PP_and (q,r))) = PP_and ((PP_or (p,q)),(PP_or (p,r)))
reconsider a = p, b = q, c = r as Element of (PartialPredConnectivesLatt D) by PARTFUN1:45;
A1: ( PP_or (p,q) = a "\/" b & PP_or (p,r) = a "\/" c ) by Def12;
PP_and (q,r) = b "/\" c by Def11;
then A2: PP_or (p,(PP_and (q,r))) = a "\/" (b "/\" c) by Def12;
PP_and ((PP_or (p,q)),(PP_or (p,r))) = (a "\/" b) "/\" (a "\/" c) by A1, Def11;
hence PP_or (p,(PP_and (q,r))) = PP_and ((PP_or (p,q)),(PP_or (p,r))) by A2, LATTICES:11; :: thesis: verum