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:88;
hence (prob A) * (prob B,A) = (prob B) * (prob A,B) by A2, XCMPLX_1:88; :: thesis: verum