set L = PartialPredConnectivesLatt D;
let x, y be Element of (PartialPredConnectivesLatt D); :: according to PARTPR_1:def 18 :: thesis: x "/\" (x `) [= y "\/" (y `)
reconsider p = x, q = y as PartialPredicate of D by PARTFUN1:46;
x ` = PP_not p by Def13;
then A1: x "/\" (x `) = PP_and (p,(PP_not p)) by Def11;
y ` = PP_not q by Def13;
then A2: y "\/" (y `) = PP_or (q,(PP_not q)) by Def12;
A3: PP_or (q,(PP_not q)) = (PP_True D) | (dom q) by Th49;
PP_and (p,(PP_not p)) = (PP_False D) | (dom p) by Th51;
then PP_or ((PP_and (p,(PP_not p))),(PP_or (q,(PP_not q)))) = PP_or (q,(PP_not q)) by A3, Th55;
hence (x "/\" (x `)) "\/" (y "\/" (y `)) = y "\/" (y `) by A1, A2, Def12; :: according to LATTICES:def 3 :: thesis: verum