let D be non empty set ; for p, q, r being PartialPredicate of D st PP_or (p,q) ||= r holds
p ||= r
let p, q, r be PartialPredicate of D; ( PP_or (p,q) ||= r implies p ||= r )
set F = PP_or (p,q);
A1:
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;
assume A2:
PP_or (p,q) ||= r
; p ||= r
let d be Element of D; NOMIN_3:def 3 ( d in dom p & p . d = TRUE implies ( d in dom r & r . d = TRUE ) )
assume
( d in dom p & p . d = TRUE )
; ( d in dom r & r . d = TRUE )
then
( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE )
by A1, PARTPR_1:def 4;
hence
( d in dom r & r . d = TRUE )
by A2; verum