let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob B holds
( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) )
let A, B be Event of E; :: thesis: ( 0 < prob B implies ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) ) )
assume A1: 0 < prob B ; :: thesis: ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) )
( (A \/ (A `)) /\ B = ([#] E) /\ B & ([#] E) /\ B = B ) by SUBSET_1:10, XBOOLE_1:28;
then (A /\ B) \/ ((A `) /\ B) = B by XBOOLE_1:23;
then (prob (A /\ B)) + (prob ((A `) /\ B)) = prob B by Th13, Th21;
then ((prob (A,B)) * (prob B)) + (prob ((A `) /\ B)) = prob B by A1, XCMPLX_1:87;
then ((prob (A,B)) * (prob B)) + ((prob ((A `),B)) * (prob B)) = prob B by A1, XCMPLX_1:87;
then (((prob (A,B)) + (prob ((A `),B))) * (prob B)) * ((prob B) ") = 1 by A1, XCMPLX_0:def 7;
then ((prob (A,B)) + (prob ((A `),B))) * ((prob B) * ((prob B) ")) = 1 ;
then ((prob (A,B)) + (prob ((A `),B))) * 1 = 1 by A1, XCMPLX_0:def 7;
hence ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) ) ; :: thesis: verum