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

per cases ( p . x = TRUE or p . x = FALSE ) by A2, PARTPR_1:3;

suppose A4: p . x = TRUE ; :: thesis: x in dom (PP_imp (p,q))

( q . x = TRUE or q . x = FALSE ) by A1, A2, PARTPR_1:3;
hence x in dom (PP_imp (p,q)) by A1, A2, A3, A4; :: thesis: verum

end;

suppose p . x = FALSE ; :: thesis: x in dom (PP_imp (p,q))

hence x in dom (PP_imp (p,q)) by A2, A3; :: thesis: verum

end;

end;