let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D st x in dom p & x in dom q & (PP_imp (p,q)) . x = TRUE & not p . x = FALSE holds
q . x = TRUE
let D be non empty set ; :: thesis: for p, q being PartialPredicate of D st x in dom p & x in dom q & (PP_imp (p,q)) . x = TRUE & not p . x = FALSE holds
q . x = TRUE
let p, q be PartialPredicate of D; :: thesis: ( x in dom p & x in dom q & (PP_imp (p,q)) . x = TRUE & not p . x = FALSE implies q . x = TRUE )
assume that
A1: x in dom p and
A2: x in dom q and
A3: (PP_imp (p,q)) . x = TRUE ; :: thesis: ( p . x = FALSE or q . x = TRUE )
( p . x <> TRUE or q . x <> FALSE ) by A1, A2, A3, Th35;
hence ( p . x = FALSE or q . x = TRUE ) by A1, A2, Th3; :: thesis: verum