let D be non empty set ; for p being PartialPredicate of D holds PP_and (p,(PP_not p)) = (PP_False D) | (dom p)
let p be PartialPredicate of D; PP_and (p,(PP_not p)) = (PP_False D) | (dom p)
set n = PP_not p;
set a = PP_and (p,(PP_not p));
set B = PP_False D;
set t = (PP_False D) | (dom p);
A1:
dom (PP_not p) = dom p
by Def2;
A2:
dom (PP_and (p,(PP_not p))) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_not p) & (PP_not p) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_not p) & (PP_not p) . d = TRUE ) ) }
by Th16;
dom (PP_False D) = D
;
then A3:
dom ((PP_False D) | (dom p)) = dom p
by RELAT_1:62;
thus A4:
dom (PP_and (p,(PP_not p))) = dom ((PP_False D) | (dom p))
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (PP_and (p,(PP_not p))) or (PP_and (p,(PP_not p))) . b1 = ((PP_False D) | (dom p)) . b1 )
let x be object ; ( not x in dom (PP_and (p,(PP_not p))) or (PP_and (p,(PP_not p))) . x = ((PP_False D) | (dom p)) . x )
assume A6:
x in dom (PP_and (p,(PP_not p)))
; (PP_and (p,(PP_not p))) . x = ((PP_False D) | (dom p)) . x
then A7: FALSE =
(PP_False D) . x
by FUNCOP_1:7
.=
((PP_False D) | (dom p)) . x
by A3, A4, A6, FUNCT_1:49
;