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 = TRUE holds
( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE )
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 = TRUE holds
( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE )
let p, q be PartialPredicate of D; :: thesis: ( x in dom (PP_and (p,q)) & (PP_and (p,q)) . x = TRUE implies ( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE ) )
assume x in dom (PP_and (p,q)) ; :: thesis: ( not (PP_and (p,q)) . x = TRUE or ( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE ) )
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 = TRUE or ( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE ) ) by Th19; :: thesis: verum