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