let D be non empty set ; :: thesis: for p, q being PartialPredicate of D st q is total holds

dom p c= dom (PP_and (p,q))

let p, q be PartialPredicate of D; :: thesis: ( q is total implies dom p c= dom (PP_and (p,q)) )

assume A1: q is total ; :: thesis: dom p c= dom (PP_and (p,q))

set a = PP_and (p,q);

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom p or x in dom (PP_and (p,q)) )

assume A2: x in dom p ; :: thesis: x in dom (PP_and (p,q))

A3: 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 PARTPR_1:16;

dom p c= dom (PP_and (p,q))

let p, q be PartialPredicate of D; :: thesis: ( q is total implies dom p c= dom (PP_and (p,q)) )

assume A1: q is total ; :: thesis: dom p c= dom (PP_and (p,q))

set a = PP_and (p,q);

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom p or x in dom (PP_and (p,q)) )

assume A2: x in dom p ; :: thesis: x in dom (PP_and (p,q))

A3: 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 PARTPR_1:16;