let E be non empty finite set ; :: thesis: for A, B being Event of E holds (prob A) + (prob ((A ` ) /\ B)) = (prob B) + (prob ((B ` ) /\ A))
let A, B be Event of E; :: thesis: (prob A) + (prob ((A ` ) /\ B)) = (prob B) + (prob ((B ` ) /\ A))
( prob A = (prob (A /\ B)) + (prob (A /\ (B ` ))) & prob B = (prob (A /\ B)) + (prob (B /\ (A ` ))) ) by Th53;
hence (prob A) + (prob ((A ` ) /\ B)) = (prob B) + (prob ((B ` ) /\ A)) ; :: thesis: verum