let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D holds
( not x in dom (PP_and (p,q)) or ( 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 ) )
let D be non empty set ; :: thesis: for p, q being PartialPredicate of D holds
( not x in dom (PP_and (p,q)) or ( 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 ) )
let p, q be PartialPredicate of D; :: thesis: ( not x in dom (PP_and (p,q)) or ( 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 ) )
assume A1: x in dom (PP_and (p,q)) ; :: thesis: ( ( 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 ) )
dom (PP_and (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) } by Th16;
then ex d1 being Element of D st
( x = d1 & ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = FALSE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = TRUE ) ) ) by A1;
hence ( ( 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 ) ) ; :: thesis: verum