set L = PartialPredConnectivesLatt D;
thus PartialPredConnectivesLatt D is de_Morgan :: thesis: ( PartialPredConnectivesLatt D is join-idempotent & PartialPredConnectivesLatt D is with_idempotent_element )
proof
let x, y be Element of (PartialPredConnectivesLatt D); :: according to ROBBINS1:def 23 :: thesis: x "/\" y = ((x `) "\/" (y `)) `
reconsider p = x, q = y as PartialPredicate of D by PARTFUN1:46;
( x ` = PP_not p & y ` = PP_not q ) by Def13;
then (x `) "\/" (y `) = PP_or ((PP_not p),(PP_not q)) by Def12;
hence ((x `) "\/" (y `)) ` = PP_and (p,q) by Def13
.= x "/\" y by Def11 ;
:: thesis: verum
end;
thus PartialPredConnectivesLatt D is join-idempotent ; :: thesis: PartialPredConnectivesLatt D is with_idempotent_element
take x = the Element of (PartialPredConnectivesLatt D); :: according to ROBBINS1:def 13 :: thesis: x "\/" x = x
thus x "\/" x = x ; :: thesis: verum