let D be non empty set ; :: thesis:
let p, q be PartialPredicate of D; :: thesis:
set o = PP_or (p,q);
set a = PP_and (p,(PP_or (p,q)));
A1: dom (PP_and (p,(PP_or (p,q)))) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE ) ) } by Th16;
A2: 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 Def4;
thus dom (PP_and (p,(PP_or (p,q)))) = dom p :: according to FUNCT_1:def 11 :: thesis:

proof

thus dom (PP_and (p,(PP_or (p,q)))) c= dom p :: according to XBOOLE_0:def 10 :: thesis:

proof

let d be object ; :: according to TARSKI:def 3 :: thesis:
assume d in dom (PP_and (p,(PP_or (p,q)))) ; :: thesis:

per cases by Th17;

suppose that A3: d in dom (PP_or (p,q)) and
A4: (PP_or (p,q)) . d = FALSE ; :: thesis:

per cases by A3, Th8;

suppose ( d in dom p & p . d = TRUE ) ; :: thesis:

hence d in dom p ; :: thesis:

end;

suppose ( ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) ; :: thesis:

hence d in dom p by A4, Def4; :: thesis:

end;

end;

end;

suppose ( ( d in dom p & p . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE ) ) ; :: thesis:

hence d in dom p ; :: thesis:

end;

end;

end;

let d be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: d in dom p ; :: thesis:

per cases by Th3;

suppose A6: p . d = TRUE ; :: thesis:

then A7: (PP_or (p,q)) . d = TRUE by A5, Def4;
d in dom (PP_or (p,q)) by A2, A5, A6;
hence d in dom (PP_and (p,(PP_or (p,q)))) by A1, A5, A6, A7; :: thesis:

end;

suppose p . d = FALSE ; :: thesis:

hence d in dom (PP_and (p,(PP_or (p,q)))) by A1, A5; :: thesis:

end;

end;

end;

let d be object ; :: thesis:
assume d in dom (PP_and (p,(PP_or (p,q)))) ; :: thesis:

per cases by Th17;

suppose that A8: d in dom (PP_or (p,q)) and
A9: (PP_or (p,q)) . d = FALSE ; :: thesis:

per cases by A8, Th8;

suppose ( d in dom p & p . d = TRUE ) ; :: thesis:

hence (PP_and (p,(PP_or (p,q)))) . d = p . d by A9, Def4; :: thesis:

end;

suppose ( d in dom q & q . d = TRUE ) ; :: thesis:

hence (PP_and (p,(PP_or (p,q)))) . d = p . d by A9, Def4; :: thesis:

end;

suppose ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ; :: thesis:

hence (PP_and (p,(PP_or (p,q)))) . d = p . d by Th19; :: thesis:

end;

end;

end;

suppose ( d in dom p & p . d = FALSE ) ; :: thesis:

hence (PP_and (p,(PP_or (p,q)))) . d = p . d by Th19; :: thesis:

end;

suppose ( d in dom p & p . d = TRUE & d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE ) ; :: thesis:

hence (PP_and (p,(PP_or (p,q)))) . d = p . d by Th18; :: thesis:

end;

end;