let D be non empty set ; :: thesis: for p being PartialPredicate of D
for a, b being Element of (PartialPredConnectivesLatt D) st a = p & b = PP_not p holds
b is_a_partial_complement_of a
let p be PartialPredicate of D; :: thesis: for a, b being Element of (PartialPredConnectivesLatt D) st a = p & b = PP_not p holds
b is_a_partial_complement_of a
set L = PartialPredConnectivesLatt D;
let a, b be Element of (PartialPredConnectivesLatt D); :: thesis: ( a = p & b = PP_not p implies b is_a_partial_complement_of a )
assume A1: ( a = p & b = PP_not p ) ; :: thesis: b is_a_partial_complement_of a
Top (PartialPredConnectivesLatt D) = PP_True D by Th60;
hence (Top (PartialPredConnectivesLatt D)) | (dom a) = PP_or ((PP_not p),p) by A1, Th49
.= b "\/" a by A1, Def12 ;
:: according to PARTPR_1:def 15 :: thesis: ( a "\/" b = (Top (PartialPredConnectivesLatt D)) | (dom a) & b "/\" a = (Bottom (PartialPredConnectivesLatt D)) | (dom a) & a "/\" b = (Bottom (PartialPredConnectivesLatt D)) | (dom a) )
hence a "\/" b = (Top (PartialPredConnectivesLatt D)) | (dom a) ; :: thesis: ( b "/\" a = (Bottom (PartialPredConnectivesLatt D)) | (dom a) & a "/\" b = (Bottom (PartialPredConnectivesLatt D)) | (dom a) )
Bottom (PartialPredConnectivesLatt D) = PP_False D by Th61;
hence (Bottom (PartialPredConnectivesLatt D)) | (dom a) = PP_and ((PP_not p),p) by A1, Th51
.= b "/\" a by A1, Def11 ;
:: thesis: a "/\" b = (Bottom (PartialPredConnectivesLatt D)) | (dom a)
hence a "/\" b = (Bottom (PartialPredConnectivesLatt D)) | (dom a) ; :: thesis: verum