let D be non empty set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: p ||= r
let d be Element of D; :: according to NOMIN_3:def 3 :: thesis: ( d in dom p & p . d = TRUE implies ( d in dom r & r . d = TRUE ) )
assume ( d in dom p & p . d = TRUE ) ; :: thesis: ( 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; :: thesis: verum