let D be non empty set ; for p, q being PartialPredicate of D holds PP_or ((PP_and (p,q)),q) = q
let p, q be PartialPredicate of D; PP_or ((PP_and (p,q)),q) = q
set a = PP_and (p,q);
set o = PP_or ((PP_and (p,q)),q);
A1:
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;
A2:
dom (PP_or ((PP_and (p,q)),q)) = { d where d is Element of D : ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom q & q . d = FALSE ) ) }
by Def4;
thus
dom (PP_or ((PP_and (p,q)),q)) = dom q
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (PP_or ((PP_and (p,q)),q)) or (PP_or ((PP_and (p,q)),q)) . b1 = q . b1 )proof
thus
dom (PP_or ((PP_and (p,q)),q)) c= dom q
XBOOLE_0:def 10 dom q c= dom (PP_or ((PP_and (p,q)),q))
let d be
object ;
TARSKI:def 3 ( not d in dom q or d in dom (PP_or ((PP_and (p,q)),q)) )
assume A5:
d in dom q
;
d in dom (PP_or ((PP_and (p,q)),q))
per cases then
( q . d = FALSE or q . d = TRUE )
by Th3;
suppose A6:
q . d = FALSE
;
d in dom (PP_or ((PP_and (p,q)),q))then A7:
(PP_and (p,q)) . d = FALSE
by A5, Th19;
d in dom (PP_and (p,q))
by A1, A5, A6;
hence
d in dom (PP_or ((PP_and (p,q)),q))
by A2, A5, A6, A7;
verum end; end;
end;
let d be object ; ( not d in dom (PP_or ((PP_and (p,q)),q)) or (PP_or ((PP_and (p,q)),q)) . d = q . d )
assume
d in dom (PP_or ((PP_and (p,q)),q))
; (PP_or ((PP_and (p,q)),q)) . d = q . d