let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D st x in dom p & p . x = TRUE & x in dom q & q . x = TRUE holds
(PP_and (p,q)) . x = TRUE
let D be non empty set ; :: thesis: for p, q being PartialPredicate of D st x in dom p & p . x = TRUE & x in dom q & q . x = TRUE holds
(PP_and (p,q)) . x = TRUE
let p, q be PartialPredicate of D; :: thesis: ( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE implies (PP_and (p,q)) . x = TRUE )
assume that
A1: x in dom p and
A2: p . x = TRUE and
A3: x in dom q and
A4: q . x = TRUE ; :: thesis: (PP_and (p,q)) . x = TRUE
A5: ( (PP_not p) . x = FALSE & (PP_not q) . x = FALSE ) by A1, A3, A2, A4, Def2;
A6: ( dom (PP_not p) = dom p & dom (PP_not q) = dom q ) by Def2;
dom (PP_or ((PP_not p),(PP_not q))) = { d where d is Element of D : ( ( d in dom (PP_not p) & (PP_not p) . d = TRUE ) or ( d in dom (PP_not q) & (PP_not q) . d = TRUE ) or ( d in dom (PP_not p) & (PP_not p) . d = FALSE & d in dom (PP_not q) & (PP_not q) . d = FALSE ) ) } by Def4;
then A7: x in dom (PP_or ((PP_not p),(PP_not q))) by A1, A3, A5, A6;
(PP_or ((PP_not p),(PP_not q))) . x = FALSE by A1, A3, A5, A6, Def4;
hence (PP_and (p,q)) . x = TRUE by A7, Def2; :: thesis: verum