let D be non empty set ; :: thesis: for p being PartialPredicate of D holds PP_or (p,(PP_not p)) = (PP_True D) | (dom p)
let p be PartialPredicate of D; :: thesis: PP_or (p,(PP_not p)) = (PP_True D) | (dom p)
set n = PP_not p;
set a = PP_or (p,(PP_not p));
set T = PP_True D;
set t = (PP_True D) | (dom p);
A1: dom (PP_not p) = dom p by Def2;
A2: dom (PP_or (p,(PP_not p))) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom (PP_not p) & (PP_not p) . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom (PP_not p) & (PP_not p) . d = FALSE ) ) } by Def4;
dom (PP_True D) = D ;
then A3: dom ((PP_True D) | (dom p)) = dom p by RELAT_1:62;
thus A4: dom (PP_or (p,(PP_not p))) = dom ((PP_True D) | (dom p)) :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (PP_or (p,(PP_not p))) or (PP_or (p,(PP_not p))) . b1 = ((PP_True D) | (dom p)) . b1 )
proof
thus dom (PP_or (p,(PP_not p))) c= dom ((PP_True D) | (dom p)) by A1, A3, Th8; :: according to XBOOLE_0:def 10 :: thesis: dom ((PP_True D) | (dom p)) c= dom (PP_or (p,(PP_not p)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((PP_True D) | (dom p)) or x in dom (PP_or (p,(PP_not p))) )
assume A5: x in dom ((PP_True D) | (dom p)) ; :: thesis: x in dom (PP_or (p,(PP_not p)))
per cases then ( p . x = TRUE or p . x = FALSE ) by A3, Th3;
suppose p . x = TRUE ; :: thesis: x in dom (PP_or (p,(PP_not p)))
hence x in dom (PP_or (p,(PP_not p))) by A2, A3, A5; :: thesis: verum
end;
suppose p . x = FALSE ; :: thesis: x in dom (PP_or (p,(PP_not p)))
then (PP_not p) . x = TRUE by A5, A3, Def2;
hence x in dom (PP_or (p,(PP_not p))) by A1, A2, A3, A5; :: thesis: verum
end;
end;
end;
let x be object ; :: thesis: ( not x in dom (PP_or (p,(PP_not p))) or (PP_or (p,(PP_not p))) . x = ((PP_True D) | (dom p)) . x )
assume A6: x in dom (PP_or (p,(PP_not p))) ; :: thesis: (PP_or (p,(PP_not p))) . x = ((PP_True D) | (dom p)) . x
then A7: TRUE = (PP_True D) . x by FUNCOP_1:7
.= ((PP_True D) | (dom p)) . x by A3, A4, A6, FUNCT_1:49 ;
per cases ( p . x = TRUE or p . x = FALSE ) by A3, A4, A6, Th3;
suppose p . x = TRUE ; :: thesis: (PP_or (p,(PP_not p))) . x = ((PP_True D) | (dom p)) . x
hence (PP_or (p,(PP_not p))) . x = ((PP_True D) | (dom p)) . x by A3, A4, A6, A7, Def4; :: thesis: verum
end;
suppose p . x = FALSE ; :: thesis: (PP_or (p,(PP_not p))) . x = ((PP_True D) | (dom p)) . x
then (PP_not p) . x = TRUE by A3, A4, A6, Def2;
hence (PP_or (p,(PP_not p))) . x = ((PP_True D) | (dom p)) . x by A1, A3, A4, A6, A7, Def4; :: thesis: verum
end;
end;