let D be non empty set ; :: thesis: for p, q, r, s being PartialPredicate of D st p ||= q & r ||= s holds
PP_or (p,r) ||= PP_or (q,s)
let p, q, r, s be PartialPredicate of D; :: thesis: ( p ||= q & r ||= s implies PP_or (p,r) ||= PP_or (q,s) )
assume that
A1: p ||= q and
A2: r ||= s ; :: thesis: PP_or (p,r) ||= PP_or (q,s)
let d be Element of D; :: according to NOMIN_3:def 3 :: thesis: ( d in dom (PP_or (p,r)) & (PP_or (p,r)) . d = TRUE implies ( d in dom (PP_or (q,s)) & (PP_or (q,s)) . d = TRUE ) )
assume A3: ( d in dom (PP_or (p,r)) & (PP_or (p,r)) . d = TRUE ) ; :: thesis: ( d in dom (PP_or (q,s)) & (PP_or (q,s)) . d = TRUE )
A4: dom (PP_or (q,s)) = { d where d is Element of D : ( ( d in dom q & q . d = TRUE ) or ( d in dom s & s . d = TRUE ) or ( d in dom q & q . d = FALSE & d in dom s & s . d = FALSE ) ) } by PARTPR_1:def 4;
( ( d in dom p & p . d = TRUE ) or ( d in dom r & r . d = TRUE ) ) by A3, PARTPR_1:10;
then ( ( d in dom q & q . d = TRUE ) or ( d in dom s & s . d = TRUE ) ) by A1, A2;
hence ( d in dom (PP_or (q,s)) & (PP_or (q,s)) . d = TRUE ) by A4, PARTPR_1:def 4; :: thesis: verum