let D be non empty set ; :: thesis: for p, q, r being PartialPredicate of D st p ||= PP_or (q,r) holds
for d being Element of D st d in dom p & p . d = TRUE & not ( d in dom q & q . d = TRUE ) holds
( d in dom r & r . d = TRUE )
let p, q, r be PartialPredicate of D; :: thesis: ( p ||= PP_or (q,r) implies for d being Element of D st d in dom p & p . d = TRUE & not ( d in dom q & q . d = TRUE ) holds
( d in dom r & r . d = TRUE ) )
assume A1: p ||= PP_or (q,r) ; :: thesis: for d being Element of D st d in dom p & p . d = TRUE & not ( d in dom q & q . d = TRUE ) holds
( d in dom r & r . d = TRUE )
let d be Element of D; :: thesis: ( d in dom p & p . d = TRUE & not ( d in dom q & q . d = TRUE ) implies ( d in dom r & r . d = TRUE ) )
assume ( d in dom p & p . d = TRUE ) ; :: thesis: ( ( d in dom q & q . d = TRUE ) or ( d in dom r & r . d = TRUE ) )
then ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) by A1;
hence ( ( d in dom q & q . d = TRUE ) or ( d in dom r & r . d = TRUE ) ) by PARTPR_1:10; :: thesis: verum