let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_and (p,q)) & (PP_and (p,q)) . x = FALSE & not ( x in dom p & p . x = FALSE ) holds
( 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_and (p,q)) & (PP_and (p,q)) . x = FALSE & not ( x in dom p & p . x = FALSE ) holds
( x in dom q & q . x = FALSE )
let p, q be PartialPredicate of D; :: thesis: ( x in dom (PP_and (p,q)) & (PP_and (p,q)) . x = FALSE & not ( x in dom p & p . x = FALSE ) implies ( x in dom q & q . x = FALSE ) )
assume x in dom (PP_and (p,q)) ; :: thesis: ( not (PP_and (p,q)) . x = FALSE or ( x in dom p & p . x = FALSE ) or ( x in dom q & q . x = FALSE ) )
then ( ( x in dom p & p . x = FALSE ) or ( x in dom q & q . x = FALSE ) or ( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE ) ) by Th17;
hence ( not (PP_and (p,q)) . x = FALSE or ( x in dom p & p . x = FALSE ) or ( x in dom q & q . x = FALSE ) ) by Th24; :: thesis: verum