:: Introduction to Probability
::  by Jan Popio{\l}ek
::
:: Received June 13, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, TARSKI,
      FINSET_1, RELAT_1, CARD_1, ARYTM_3, XXREAL_0, REAL_1, ARYTM_1, RPR_1,
      BSPACE;
 notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, DOMAIN_1, CARD_1, NUMBERS,
      XCMPLX_0, REAL_1, FINSEQ_1, FINSET_1, XXREAL_0;
 constructors XXREAL_0, REAL_1, NAT_1, MEMBERED, FINSEQ_1, DOMAIN_1;
 registrations XBOOLE_0, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, MEMBERED,
      SUBSET_1, CARD_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions XBOOLE_0, SUBSET_1;
 theorems TARSKI, SUBSET_1, ZFMISC_1, FINSEQ_1, CARD_1, CARD_2,
      XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XREAL_0, NAT_1;

begin

reserve E for non empty set;
reserve a for Element of E;
reserve A, B for Subset of E;
reserve Y for set;
reserve p for FinSequence;

theorem Th1:
  for e being non empty Subset of E holds e is Singleton of E iff for Y
  holds (Y c= e iff Y = {} or Y = e)
proof
  let e be non empty Subset of E;
  thus e is Singleton of E implies for Y holds (Y c= e iff Y = {} or Y = e)
  proof
    assume
A1: e is Singleton of E;
    let Y;
    ex x being set st e = {x} by A1,ZFMISC_1:131;
    hence thesis by ZFMISC_1:33;
  end;
  assume
A2: for Y holds Y c= e iff Y = {} or Y = e;
  consider x being set such that
A3: x in e by XBOOLE_0:def 1;
  {x} c= e by A3,ZFMISC_1:31;
  hence thesis by A2;
end;

registration
  let E;
  cluster -> finite for Singleton of E;
  coherence;
end;

reserve e, e1, e2 for Singleton of E;

theorem
  e = A \/ B & A <> B implies A = {} & B = e or A = e & B = {}
proof
  assume that
A1: e = A \/ B and
A2: A <> B;
  A c= e by A1,XBOOLE_1:7;
  then
A3: A = {} or A = e by Th1;
  B c= e by A1,XBOOLE_1:7;
  hence thesis by A2,A3,Th1;
end;

theorem
  e = A \/ B implies A = e & B = e or A = e & B = {} or A = {} & B = e
proof
  assume
A1: e = A \/ B;
  then A c= e & B c= e by XBOOLE_1:7;
  then
  A = {} & B = e or A = e & B = {} or A = e & B = e or A = {} & B = {} by Th1;
  hence thesis by A1;
end;

theorem
  {a} is Singleton of E;

theorem
  e1 c= e2 implies e1 = e2 by Th1;

theorem Th6:
  ex a st a in E & e = {a}
proof
  set x = the Element of e;
  {x} = e by Th1;
  hence thesis;
end;

theorem
  ex e st e is Singleton of E
proof
  take {the Element of E};
  thus thesis;
end;

theorem
  ex p st p is FinSequence of E & rng p = e & len p = 1
proof
  consider a such that
  a in E and
A1: e = {a} by Th6;
  rng <*a*> = {a} & len <*a*> = 1 by FINSEQ_1:39;
  hence thesis by A1;
end;

definition
  let E be set;
  mode Event of E is Subset of E;
end;

theorem
  for E being non empty set, e being Singleton of E, A being Event of E
  holds e misses A or e /\ A = e
proof
  let E be non empty set, e be Singleton of E, A be Event of E;
  e /\ E = e & A \/ A` = [#] E by SUBSET_1:10,XBOOLE_1:28;
  then e = e /\ A \/ e /\ A` by XBOOLE_1:23;
  then e /\ A c= e by XBOOLE_1:7;
  then e /\ A = {} or e /\ A = e by Th1;
  hence thesis by XBOOLE_0:def 7;
end;

theorem
  for E being non empty set, A being Event of E st A <> {} ex e being
  Singleton of E st e c= A
proof
  let E be non empty set, A be Event of E;
  set x = the Element of A;
  assume
A1: A <> {};
  then reconsider x as Element of E by TARSKI:def 3;
  {x} c= A by A1,ZFMISC_1:31;
  hence thesis;
end;

theorem
  for E being non empty set, e being Singleton of E, A being Event of E st e
  c= A \/ A` holds e c= A or e c= A`
proof
  let E be non empty set, e be Singleton of E, A be Event of E;
  ex a being Element of E st a in E & e = {a} by Th6;
  then consider a being Element of E such that
A1: e = {a};
  assume e c= A \/ A`;
  then a in A \/ A` by A1,ZFMISC_1:31;
  then a in A or a in A` by XBOOLE_0:def 3;
  hence thesis by A1,ZFMISC_1:31;
end;

theorem
  e1 = e2 or e1 misses e2
proof
  e1 /\ e2 c= e1 by XBOOLE_1:17;
  then e1 /\ e2 = {} or e1 /\ e2 = e1 by Th1;
  then e1 c= e2 or e1 /\ e2 = {} by XBOOLE_1:17;
  hence thesis by Th1,XBOOLE_0:def 7;
end;

theorem Th13:
  A /\ B misses A /\ B`
proof
  A /\ B misses A \ B by XBOOLE_1:89;
  hence thesis by SUBSET_1:13;
end;

Lm1: for E being finite non empty set holds 0 < card E
proof
  let E be finite non empty set;
  card {the Element of E} <= card E by NAT_1:43;
  hence thesis by CARD_1:30;
end;

definition
  let E be finite set;
  let A be Event of E;
  func prob(A) -> Real equals
  card A / card E;
  coherence by XREAL_0:def 1;
end;

theorem
  for E being finite non empty set, e being Singleton of E holds prob(e) = 1
  / card E by CARD_1:def 7;

theorem
  for E being finite non empty set holds prob([#] E) = 1 by XCMPLX_1:60;

theorem Th16:
  for E being finite non empty set, A,B being Event of E st A
  misses B holds prob(A /\ B) = 0
proof
  let E be finite non empty set, A,B be Event of E;
  assume A misses B;
  then A /\ B = {} E by XBOOLE_0:def 7;
  hence thesis by CARD_1:27;
end;

theorem
  for E being finite non empty set, A being Event of E holds prob(A) <= 1
proof
  let E be finite non empty set, A be Event of E;
  0 < card E by Lm1;
  then card A * (card E)" <= card E * (card E)" by NAT_1:43,XREAL_1:64;
  then card A / card E <= card E * (card E)" by XCMPLX_0:def 9;
  then prob([#] E) = card E / card E & prob(A) <= card E / card E by
XCMPLX_0:def 9;
  hence thesis by XCMPLX_1:60;
end;

theorem Th18:
  for E being finite non empty set, A being Event of E holds 0 <= prob(A)
proof
  let E be finite non empty set, A be Event of E;
  0 < card E & 0 <= card A by Lm1,CARD_1:27;
  hence thesis;
end;

theorem Th19:
  for E being finite non empty set, A,B being Event of E st A c= B
  holds prob(A) <= prob(B)
proof
  let E be finite non empty set, A,B be Event of E;
  assume
A1: A c= B;
  0 < card E by Lm1;
  then card A * (card E)" <= card B * (card E)" by A1,NAT_1:43,XREAL_1:64;
  then card A / card E <= card B * (card E)" by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem Th20:
  for E being finite non empty set, A,B being Event of E holds
  prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B)
proof
  let E be finite non empty set, A,B be Event of E;
  set q = ( card E )";
  set p = card E;
  card (( A \/ B ) qua Event of E) = card A + card B - card ( A /\ B ) by
CARD_2:45;
  then
  card ( A \/ B ) * q = card A * q + ( card B * q - card ( A /\ B ) * q );
  then card ( A \/ B ) / p = card A * q + card B * q - card ( A /\ B ) * q by
XCMPLX_0:def 9;
  then card ( A \/ B ) / p = card A / p + card B * q - card ( A /\ B ) * q by
XCMPLX_0:def 9;
  then card ( A \/ B ) / p = card A / p + card B / p - card ( A /\ B ) * q by
XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem Th21:
  for E being finite non empty set, A,B being Event of E st A
  misses B holds prob(A \/ B) = prob(A) + prob(B)
proof
  let E be finite non empty set, A,B be Event of E;
  assume A misses B;
  then prob(A /\ B) = 0 by Th16;
  then prob(A \/ B) = prob(A) + prob(B) - 0 by Th20;
  hence thesis;
end;

theorem Th22:
  for E being finite non empty set, A being Event of E holds prob(
  A) = 1 - prob(A`) & prob(A`) = 1 - prob(A)
proof
  let E be finite non empty set, A be Event of E;
  A misses A` by SUBSET_1:24;
  then prob(A \/ A`) = prob(A) + prob(A`) by Th21;
  then prob( [#] E ) = prob(A) + prob(A`) by SUBSET_1:10;
  then 1 = prob(A) + prob(A`) by XCMPLX_1:60;
  hence thesis;
end;

theorem Th23:
  for E being finite non empty set, A,B being Event of E holds
  prob(A \ B) = prob(A) - prob(A /\ B)
proof
  let E be finite non empty set, A,B be Event of E;
  prob(A) = prob((A \ B) \/ (A /\ B)) by XBOOLE_1:51;
  then prob(A) = prob(A \ B) + prob(A /\ B) by Th21,XBOOLE_1:89;
  hence thesis;
end;

theorem Th24:
  for E being finite non empty set, A,B being Event of E st B c= A
  holds prob(A \ B) = prob(A) - prob(B)
proof
  let E be finite non empty set, A,B be Event of E;
  assume B c= A;
  then prob(A /\ B) = prob(B) by XBOOLE_1:28;
  hence thesis by Th23;
end;

theorem
  for E being finite non empty set, A,B being Event of E holds prob(A \/
  B) <= prob(A) + prob(B)
proof
  let E be finite non empty set, A,B be Event of E;
  prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B) by Th20;
  hence thesis by Th18,XREAL_1:43;
end;

theorem Th26:
  for E being finite non empty set, A,B being Event of E holds
  prob(A) = prob(A /\ B) + prob(A /\ B`)
proof
  let E be finite non empty set, A,B be Event of E;
  A = A /\ ( A \/ [#] E ) by XBOOLE_1:21;
  then A = A /\ [#] E by SUBSET_1:11;
  then
A1: A = A /\ ( B \/ B`) by SUBSET_1:10;
  prob((A /\ B) \/ (A /\ B`)) = prob(A /\ B) + prob(A /\ B`) by Th13,Th21;
  hence thesis by A1,XBOOLE_1:23;
end;

theorem
  for E being finite non empty set, A,B being Event of E holds prob(A) =
  prob(A \/ B) - prob(B \ A)
proof
  let E be finite non empty set, A,B be Event of E;
  prob(A \/ (B \ A)) = prob(A \/ B) by XBOOLE_1:39;
  then prob(A \/ B) = prob(A) + prob(B \ A) by Th21,XBOOLE_1:79;
  hence thesis;
end;

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

theorem Th29:
  for E being finite non empty set, A,B,C being Event of E holds
  prob(A \/ B \/ C) = ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A
  /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C)
proof
  let E be finite non empty set, A,B,C be Event of E;
  prob(A \/ B \/ C) = prob(A \/ B) + prob(C) - prob((A \/ B) /\ C) by Th20
    .= ( ( prob(A) + prob(B) ) - prob(A /\ B) ) + prob(C) - prob((A \/ B) /\
  C) by Th20
    .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - prob((A /\ C) \/ (B
  /\ C)) by XBOOLE_1:23
    .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - ( prob(A /\ C) +
  prob(B /\ C) - prob((A /\ C) /\ (B /\ C)) ) by Th20
    .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - ( prob(A /\ C) +
  prob(B /\ C) - prob(A /\ ( C /\ (C /\ B)) )) by XBOOLE_1:16
    .= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) - ( prob(A /\ C) +
  prob(B /\ C) - prob(A /\ (( C /\ C ) /\ B) )) by XBOOLE_1:16
    .= (( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B)) - ( prob(A /\ C) +
  prob(B /\ C) - prob(A /\ B /\ C) ) by XBOOLE_1:16
    .= ( prob(A) + prob(B) + prob(C) ) + -( prob(A /\ B) + prob(A /\ C) +
  prob(B /\ C) ) + prob(A /\ B /\ C);
  hence thesis;
end;

theorem
  for E being finite non empty set, A,B,C being Event of E st A misses B
& A misses C & B misses C holds prob(A \/ B \/ C) = prob(A) + prob(B) + prob(C)
proof
  let E be finite non empty set, A,B,C be Event of E;
  assume that
A1: A misses B and
A2: A misses C and
A3: B misses C;
A4: prob(A /\ (B /\ C)) = 0 by A1,Th16,XBOOLE_1:74;
  prob(A \/ B \/ C) = ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) +
  prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) by Th29
    .= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) +
  prob(B /\ C) ) + 0 by A4,XBOOLE_1:16
    .= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) + 0 )
  by A3,Th16
    .= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + 0 ) by A2,Th16
    .= ( prob(A) + prob(B) + prob(C) ) - 0 by A1,Th16;
  hence thesis;
end;

theorem
  for E being finite non empty set, A,B being Event of E holds prob(A) -
  prob(B) <= prob(A \ B)
proof
  let E be finite non empty set, A,B be Event of E;
  prob(A /\ B) <= prob(B) by Th19,XBOOLE_1:17;
  then prob(A) - prob(B) <= prob(A) - prob(A /\ B) by XREAL_1:13;
  hence thesis by Th23;
end;

definition
  let E be finite set;
  let B,A be Event of E;
  func prob(A, B) -> Real equals
  prob(A /\ B) / prob(B);
  coherence;
end;

theorem
  for E being finite non empty set, A being Event of E holds
  prob(A, [#]E ) = prob(A)
proof
  let E be finite non empty set, A be Event of E;
  prob([#] E) = 1 by XCMPLX_1:60;
  hence thesis by XBOOLE_1:28;
end;

theorem
  for E being finite non empty set holds prob([#] E, [#] E) = 1
proof
  let E be finite non empty set;
  prob([#] E) = 1 by XCMPLX_1:60;
  hence thesis;
end;

theorem
  for E being finite non empty set, A,B being Event of E st 0 < prob(B)
  holds prob(A, B) <= 1
proof
  let E be finite non empty set, A,B be Event of E;
  assume
A1: 0 < prob(B);
  A /\ B c= B by XBOOLE_1:17;
  then prob(A /\ B) * (prob(B))" <= prob(B) * (prob(B))" by A1,Th19,XREAL_1:64;
  then prob(A /\ B) * (prob(B))" <= 1 by A1,XCMPLX_0:def 7;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  for E being finite non empty set, A,B being Event of E st 0 < prob(B)
  holds 0 <= prob(A, B)
proof
  let E be finite non empty set, A,B be Event of E;
  assume
A1: 0 < prob(B);
  0 <= prob(A /\ B) by Th18;
  hence thesis by A1;
end;

theorem Th36:
  for E being finite non empty set, A,B being Event of E st 0 <
  prob(B) holds prob(A, B) = 1 - prob(B \ A) / prob(B)
proof
  let E be finite non empty set, A,B be Event of E;
  prob(B \ A) + prob(A /\ B) = ( prob(B) - prob(A /\ B) ) + prob(A /\ B)
  by Th23;
  then prob(A, B) = ( prob(B) - prob(B \ A) ) / prob(B);
  then
A1: prob(A, B) = prob(B) / prob(B) - prob(B \ A) / prob(B) by XCMPLX_1:120;
  assume 0 < prob(B);
  hence thesis by A1,XCMPLX_1:60;
end;

theorem
  for E being finite non empty set, A,B being Event of E st 0 < prob(B)
  & A c= B holds prob(A, B) = prob(A) / prob(B)
proof
  let E be finite non empty set, A,B be Event of E;
  assume that
A1: 0 < prob(B) and
A2: A c= B;
  prob(A, B) = 1 - prob(B \ A) / prob(B) by A1,Th36;
  then prob(A, B) = 1 - ( prob(B) - prob(A) ) / prob(B) by A2,Th24;
  then prob(A, B) = 1 - ( prob(B) / prob(B) - prob(A) / prob(B) ) by
XCMPLX_1:120;
  then prob(A, B) = 1 - ( 1 - prob(A) / prob(B) ) by A1,XCMPLX_1:60;
  hence thesis;
end;

theorem Th38:
  for E being finite non empty set, A,B being Event of E st A
  misses B holds prob(A, B) = 0
proof
  let E be finite non empty set, A,B be Event of E;
  assume A misses B;
  then prob(A, B) = 0 / prob(B) by Th16
    .= 0 * (prob(B))";
  hence thesis;
end;

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

theorem Th40:
  for E being finite non empty set, 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)
proof
  let E be finite non empty set, A,B be Event of E;
  assume
A1: 0 < prob(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 thesis;
end;

theorem Th41:
  for E being finite non empty set, A,B being Event of E st 0 <
  prob(B) & B c= A holds prob(A, B) = 1
proof
  let E be finite non empty set, A,B be Event of E;
  assume that
A1: 0 < prob(B) and
A2: B c= A;
  prob(A /\ B) = prob(B) by A2,XBOOLE_1:28;
  hence thesis by A1,XCMPLX_1:60;
end;

theorem
  for E being finite non empty set, B being Event of E st 0 < prob(B)
  holds prob([#] E, B) = 1 by Th41;

theorem
  for E being finite non empty set, A being Event of E holds prob(A`, A) = 0
proof
  let E be finite non empty set, A be Event of E;
  A` misses A by SUBSET_1:24;
  then prob(A` /\ A) = 0 by Th16;
  hence thesis;
end;

theorem
  for E being finite non empty set, A being Event of E holds prob(A, A`) = 0
proof
  let E be finite non empty set, A be Event of E;
  A misses A` by SUBSET_1:24;
  then prob(A /\ A`) = 0 by Th16;
  hence thesis;
end;

theorem Th45:
  for E being finite non empty set, A,B being Event of E st 0 <
  prob(B) & A misses B holds prob(A`, B) = 1
proof
  let E be finite non empty set, A,B be Event of E;
  assume that
A1: 0 < prob(B) and
A2: A misses B;
  prob(A, B) = 0 by A2,Th38;
  then 1 - prob(A`, B) = 0 by A1,Th40;
  hence thesis;
end;

theorem Th46:
  for E being finite non empty set, A,B being Event of E st 0 <
prob(A) & prob(B) < 1 & A misses B holds prob(A, B`) = prob(A) / (1 - prob(B))
proof
  let E be finite non empty set, A,B be Event of E;
  assume that
A1: 0 < prob(A) and
A2: prob(B) < 1 and
A3: A misses B;
  prob(B) - 1 < 1 - 1 by A2,XREAL_1:9;
  then 0 < - ( - ( 1 - prob(B) ) );
  then
A4: 0 < prob(B`) by Th22;
  then prob(A) * prob(B`, A) = prob(B`) * prob(A, B`) by A1,Th39;
  then prob(A) * 1 = prob(B`) * prob(A, B`) by A1,A3,Th45;
  then prob(A) * (prob(B`))" = prob(A, B`) * ( prob(B`) * (prob(B`))" );
  then
A5: prob(A) * (prob(B`))" = prob(A, B`) * 1 by A4,XCMPLX_0:def 7;
  prob(B`) = 1 - prob(B) by Th22;
  hence thesis by A5,XCMPLX_0:def 9;
end;

theorem
  for E being finite non empty set, A,B being Event of E st 0 < prob(A)
  & prob(B) < 1 & A misses B holds prob(A`, B`) = 1 - prob(A) / (1 - prob(B))
proof
  let E be finite non empty set, A,B be Event of E;
  assume that
A1: 0 < prob(A) and
A2: prob(B) < 1 and
A3: A misses B;
A4: prob(B`) = 1 - prob(B) by Th22;
  prob(B) -1 < 1 - 1 by A2,XREAL_1:9;
  then 0 < - ( - ( 1 - prob(B) ) );
  then prob(A` , B`) = 1 - prob(A, B`) by A4,Th40;
  hence thesis by A1,A2,A3,Th46;
end;

theorem
  for E being finite non empty set, A,B,C being Event of E st 0 < prob(B
  /\ C) & 0 < prob(C) holds prob(A /\ B /\ C) = prob(A, B /\ C) * prob(B, C) *
  prob(C)
proof
  let E be finite non empty set, A,B,C be Event of E;
  assume that
A1: 0 < prob(B /\ C) and
A2: 0 < prob(C);
A3: prob(B /\ C) = prob(B, C) * prob(C) by A2,XCMPLX_1:87;
  prob(A /\ B /\ C) = prob(A /\ (B /\ C)) by XBOOLE_1:16;
  then prob(A /\ B /\ C) = prob(A, B /\ C) * prob(B /\ C) by A1,XCMPLX_1:87;
  hence thesis by A3;
end;

theorem Th49:
  for E being finite non empty set, A,B being Event of E st 0 <
prob(B) & prob(B) < 1 holds prob(A) = prob(A, B) * prob(B) + prob(A, B`) * prob
  (B`)
proof
  let E be finite non empty set, A,B be Event of E;
  assume that
A1: 0 < prob(B) and
A2: prob(B) < 1;
  prob(B) -1 < 1 - 1 by A2,XREAL_1:9;
  then 0 < - ( - ( 1 - prob(B) ) );
  then
A3: 0 < prob(B`) by Th22;
  prob(A) = prob(A /\ B) + prob(A /\ B`) by Th26;
  then prob(A) = prob(A, B) * prob(B) + prob(A /\ B`) by A1,XCMPLX_1:87;
  hence thesis by A3,XCMPLX_1:87;
end;

theorem Th50:
  for E being finite non empty set, A,B1,B2 being Event of E st 0
< prob(B1) & 0 < prob(B2) & B1 \/ B2 = E & B1 misses B2 holds prob(A) = prob(A,
  B1) * prob(B1) + prob(A, B2) * prob(B2)
proof
  let E be finite non empty set, A,B1,B2 be Event of E;
  assume that
A1: 0 < prob(B1) and
A2: 0 < prob(B2) and
A3: B1 \/ B2 = E and
A4: B1 misses B2;
A5: B2 \ B1 = E \ B1 by A3,XBOOLE_1:40;
  then 0 < prob((B1)`) by A2,A4,XBOOLE_1:83;
  then 0 < 1 - prob(B1) by Th22;
  then
A6: 1 - ( 1 - prob(B1) ) < 1 by XREAL_1:44;
  B2 = B1` by A4,A5,XBOOLE_1:83;
  hence thesis by A1,A6,Th49;
end;

theorem Th51:
  for E being finite non empty set, A,B1,B2,B3 being Event of E st
0 < prob(B1) & 0 < prob(B2) & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2
& B1 misses B3 & B2 misses B3 holds prob(A) = ( prob(A, B1) * prob(B1) + prob(A
  , B2) * prob(B2) ) + prob(A, B3) * prob(B3)
proof
  let E be finite non empty set, A,B1,B2,B3 be Event of E;
  assume that
A1: 0 < prob(B1) and
A2: 0 < prob(B2) and
A3: 0 < prob(B3) and
A4: B1 \/ B2 \/ B3 = E and
A5: B1 /\ B2 = {} and
A6: B1 /\ B3 = {} and
A7: B2 /\ B3 = {};
  (B1 /\ B3) \/ (B2 /\ B3) = B2 /\ B3 by A6;
  then (B1 \/ B2) /\ B3 = {} by A7,XBOOLE_1:23;
  then
A8: (B1 \/ B2) misses B3 by XBOOLE_0:def 7;
  (B1 \/ B2 \/ B3) /\ A = A by A4,XBOOLE_1:28;
  then ((B1 \/ B2) /\ A) \/ (B3 /\ A) = A by XBOOLE_1:23;
  then prob(A) = prob((B1 \/ B2) /\ A) + prob(B3 /\ A) by A8,Th21,XBOOLE_1:76;
  then
A9: prob(A) = prob((B1 /\ A) \/ (B2 /\ A)) + prob(B3 /\ A) by XBOOLE_1:23;
  B1 misses B2 by A5,XBOOLE_0:def 7;
  then prob(A) = prob(A /\ B1) + prob(A /\ B2) + prob(A /\ B3) by A9,Th21,
XBOOLE_1:76;
  then
  prob(A) = prob(A, B1) * prob(B1) + prob(A /\ B2) + prob(A /\ B3) by A1,
XCMPLX_1:87;
  then prob(A) = prob(A, B1) * prob(B1) + prob(A, B2) * prob(B2) + prob(A /\
  B3) by A2,XCMPLX_1:87;
  hence thesis by A3,XCMPLX_1:87;
end;

theorem
  for E being finite non empty set, A,B1,B2 being Event of E st 0 < prob
(B1) & 0 < prob(B2) & B1 \/ B2 = E & B1 misses B2 holds prob(B1, A) = ( prob(A,
  B1) * prob(B1) ) / ( prob(A, B1) * prob(B1) + prob(A, B2) * prob(B2) )
proof
  let E be finite non empty set, A,B1,B2 be Event of E;
  assume that
A1: 0 < prob(B1) and
A2: 0 < prob(B2) & B1 \/ B2 = E & B1 misses B2;
  prob(A) = prob(A, B1) * prob(B1) + prob(A, B2) * prob(B2) by A1,A2,Th50;
  hence thesis by A1,XCMPLX_1:87;
end;

theorem
  for E being finite non empty set, A,B1,B2,B3 being Event of E st 0 <
prob(B1) & 0 < prob(B2) & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2 & B1
  misses B3 & B2 misses B3 holds prob(B1, A) = ( prob(A, B1) * prob(B1) ) / ( (
  prob(A, B1) * prob(B1) + prob(A, B2) * prob(B2) ) + prob(A, B3) * prob(B3) )
proof
  let E be finite non empty set, A,B1,B2,B3 be Event of E;
  assume that
A1: 0 < prob(B1) and
A2: 0 < prob(B2) & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2 & B1
  misses B3 & B2 misses B3;
  prob(A) = ( prob(A, B1) * prob(B1) + prob(A, B2) * prob(B2) ) + prob(A,
  B3) * prob(B3) by A1,A2,Th51;
  hence thesis by A1,XCMPLX_1:87;
end;

definition
  let E be finite set;
  let A, B be Event of E;
  pred A, B are_independent means
  :Def3:
  prob(A /\ B) = prob(A) * prob(B);
  symmetry;
end;

theorem
  for E being finite non empty set, A,B being Event of E st 0 < prob(B)
  & A, B are_independent holds prob(A, B) = prob(A)
proof
  let E be finite non empty set, A,B be Event of E;
  assume that
A1: 0 < prob(B) and
A2: A, B are_independent;
  prob(A /\ B) = prob(A) * prob(B) by A2,Def3;
  then prob(A, B) = prob(A) * ( prob(B) / prob(B) ) by XCMPLX_1:74;
  then prob(A, B) = prob(A) * 1 by A1,XCMPLX_1:60;
  hence thesis;
end;

theorem
  for E being finite non empty set, A,B being Event of E st prob(B) = 0
  holds A, B are_independent
proof
  let E be finite non empty set, A,B be Event of E;
A1: 0 = prob(A) * 0;
  assume
A2: prob(B) = 0;
  then prob(A /\ B) <= 0 by Th19,XBOOLE_1:17;
  then prob(A /\ B) = 0 by Th18;
  hence thesis by A2,A1,Def3;
end;

theorem
  for E being finite non empty set, A,B being Event of E st A, B
  are_independent holds A`, B are_independent
proof
  let E be finite non empty set, A,B be Event of E;
  prob(A` /\ B) = prob(B \ A) by SUBSET_1:13;
  then
A1: prob(A` /\ B) = prob(B) - prob(A /\ B) by Th23;
  assume A, B are_independent;
  then prob(A` /\ B) = 1 * prob(B) - prob(A) * prob(B) by A1,Def3;
  then prob(A` /\ B) = ( 1 - prob(A) ) * prob(B);
  then prob(A` /\ B) = prob(A`) * prob(B) by Th22;
  hence thesis by Def3;
end;

theorem
  for E being finite non empty set, A,B being Event of E st A misses B &
  A, B are_independent holds prob(A) = 0 or prob(B) = 0
proof
  let E be finite non empty set, A,B be Event of E;
  assume that
A1: A misses B and
A2: A, B are_independent;
  prob(A /\ B) = 0 by A1,Th16;
  then prob(A) * prob(B) = 0 by A2,Def3;
  hence thesis by XCMPLX_1:6;
end;