let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob A & 0 < prob B holds
(prob A) * (prob (B,A)) = (prob B) * (prob (A,B))
let A, B be Event of E; :: thesis: ( 0 < prob A & 0 < prob B implies (prob A) * (prob (B,A)) = (prob B) * (prob (A,B)) )
assume that
A1: 0 < prob A and
A2: 0 < prob B ; :: thesis: (prob A) * (prob (B,A)) = (prob B) * (prob (A,B))
(prob A) * (prob (B,A)) = prob (A /\ B) by A1, XCMPLX_1:87;
hence (prob A) * (prob (B,A)) = (prob B) * (prob (A,B)) by A2, XCMPLX_1:87; :: thesis: verum