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