let D be non empty set ; :: thesis: for p, q, r being PartialPredicate of D st p ||= r holds
PP_and (p,q) ||= r
let p, q, r be PartialPredicate of D; :: thesis: ( p ||= r implies PP_and (p,q) ||= r )
set F = PP_and (p,q);
A1: dom (PP_and (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) } by PARTPR_1:16;
assume A2: p ||= r ; :: thesis: PP_and (p,q) ||= r
let d be Element of D; :: according to NOMIN_3:def 3 :: thesis: ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE implies ( d in dom r & r . d = TRUE ) )
assume that
A3: d in dom (PP_and (p,q)) and
A4: (PP_and (p,q)) . d = TRUE ; :: thesis: ( d in dom r & r . d = TRUE )
consider d1 being Element of D such that
A5: d = d1 and
A6: ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = FALSE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = TRUE ) ) by A1, A3;
per cases ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = FALSE ) or ( d1 in dom p & d1 in dom q & p . d1 = TRUE & q . d1 = TRUE ) ) by A6;
suppose ( d1 in dom p & p . d1 = FALSE ) ; :: thesis: ( d in dom r & r . d = TRUE )
hence ( d in dom r & r . d = TRUE ) by A4, A5, PARTPR_1:19; :: thesis: verum
end;
suppose ( d1 in dom q & q . d1 = FALSE ) ; :: thesis: ( d in dom r & r . d = TRUE )
hence ( d in dom r & r . d = TRUE ) by A4, A5, PARTPR_1:19; :: thesis: verum
end;
suppose ( d1 in dom p & d1 in dom q & p . d1 = TRUE & q . d1 = TRUE ) ; :: thesis: ( d in dom r & r . d = TRUE )
hence ( d in dom r & r . d = TRUE ) by A2, A5; :: thesis: verum
end;
end;