let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_imp (p,q)) & (PP_imp (p,q)) . x = FALSE holds
( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE )
let D be non empty set ; :: thesis: for p, q being PartialPredicate of D st x in dom (PP_imp (p,q)) & (PP_imp (p,q)) . x = FALSE holds
( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE )
let p, q be PartialPredicate of D; :: thesis: ( x in dom (PP_imp (p,q)) & (PP_imp (p,q)) . x = FALSE implies ( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE ) )
assume x in dom (PP_imp (p,q)) ; :: thesis: ( not (PP_imp (p,q)) . x = FALSE or ( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE ) )
then ( ( x in dom p & p . x = FALSE ) or ( x in dom q & q . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE ) ) by Th32;
hence ( not (PP_imp (p,q)) . x = FALSE or ( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE ) ) by Th33, Def4; :: thesis: verum