let D be non empty set ; :: thesis: for p, q being PartialPredicate of D st q is total holds
dom p c= dom (PP_or (p,q))
let p, q be PartialPredicate of D; :: thesis: ( q is total implies dom p c= dom (PP_or (p,q)) )
assume A1: q is total ; :: thesis: dom p c= dom (PP_or (p,q))
set a = PP_or (p,q);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom p or x in dom (PP_or (p,q)) )
assume A2: x in dom p ; :: thesis: x in dom (PP_or (p,q))
A3: dom (PP_or (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } by PARTPR_1:def 4;