let x be object ; 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 ; 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; ( 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))
; ( 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; verum