:: The Fundamental Logic Structure in Quantum Mechanics
::  by Pawe{\l} Sadowski, Andrzej Trybulec and Konrad Raczkowski
::
:: Received December 18, 1989
:: 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, SUBSET_1, XBOOLE_0, RPR_1, PROB_1, FUNCT_2, FUNCT_1,
      ZFMISC_1, CARD_1, XXREAL_0, TARSKI, ARYTM_3, RELAT_1, SEQ_2, ORDINAL2,
      EQREL_1, REAL_1, ARYTM_1, STRUCT_0, ORDERS_2, ROBBINS1, ORDERS_1,
      MCART_1, XBOOLEAN, CQC_THE1, ZFREFLE1, RELAT_2, QMAX_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1,
      XTUPLE_0, SUBSET_1, NUMBERS, RELAT_1, RELSET_1,
      RELAT_2, FUNCT_1, REAL_1, FUNCT_2, ORDERS_1, DOMAIN_1, SEQ_2, PROB_1,
      MCART_1, EQREL_1, XXREAL_0, STRUCT_0, ORDERS_2, ROBBINS1;
 constructors DOMAIN_1, XXREAL_0, EQREL_1, SEQ_2, PROB_1, ORDERS_2, ROBBINS1,
      REAL_1, SEQ_1, VALUED_1, RELSET_1, FINSUB_1, COMSEQ_2, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, NUMBERS,
      MEMBERED, EQREL_1, PROB_1, RELAT_1, FUNCT_1, XTUPLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions RELAT_2, ORDERS_1, SUBSET_1, XTUPLE_0;
 theorems ORDERS_1, TARSKI, FUNCT_1, ZFMISC_1, FUNCT_2, PROB_1, MCART_1,
      EQREL_1, RELAT_1, RELSET_1, XBOOLE_0, XREAL_1, XXREAL_0, NAT_1;
 schemes EQREL_1, RELSET_1, FUNCT_2, XBOOLE_0;

begin

reserve X1,x,y,z for set,
  n,m for Element of NAT,
  X for non empty set;
reserve A,B for Event of Borel_Sets,
  D for Subset of REAL;

definition let X;
  let S be SigmaField of X;
  func Probabilities(S) -> set means
  :Def1:
  x in it iff x is Probability of S;
  existence
  proof
    defpred P[set] means $1 is Probability of S;
    consider X being set such that
A1: x in X iff x in Funcs(S,REAL) & P[x] from XBOOLE_0:sch 1;
    take X;
    let x;
    x is Probability of S implies x in Funcs(S,REAL) by FUNCT_2:8;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let A1,A2 be set;
    assume that
A2: x in A1 iff x is Probability of S and
A3: x in A2 iff x is Probability of S;
    now
      let y;
      y in A1 iff y is Probability of S by A2;
      hence y in A1 iff y in A2 by A3;
    end;
    hence thesis by TARSKI:1;
  end;
end;

registration let X;
  let S be SigmaField of X;
  cluster Probabilities(S) -> non empty;
  coherence
  proof
    set x = the Probability of S;
    x in Probabilities(S) by Def1;
    hence thesis;
  end;
end;

definition
  struct QM_Str (# Observables, FStates -> non empty set,
     Quantum_Probability -> Function of [:the Observables, the FStates:],
       Probabilities(Borel_Sets) #);
end;

reserve Q for QM_Str;

definition let Q;
  func Obs Q -> set equals
  the Observables of Q;
  coherence;
  func Sts Q -> set equals
  the FStates of Q;
  coherence;
end;

registration let Q;
  cluster Obs Q -> non empty;
  coherence;
  cluster Sts Q -> non empty;
  coherence;
end;

reserve A1 for Element of Obs Q;
reserve s for Element of Sts Q;
reserve E for Event of Borel_Sets;
reserve ASeq for SetSequence of Borel_Sets;

definition let Q,A1,s;
  func Meas(A1,s) -> Probability of Borel_Sets equals
  (the Quantum_Probability of Q).[A1,s];
  coherence
  proof
    reconsider A1s = [A1,s] as Element of [:the Observables of Q,
    the FStates of Q:];
    (the Quantum_Probability of Q).A1s is Element of Probabilities Borel_Sets;
    hence thesis by Def1;
  end;
end;

set X = {0};
consider P being Function of Borel_Sets,REAL such that
Lm1: for D st D in Borel_Sets holds (0 in D implies P.D = 1) & (not 0 in D
implies P.D = 0) by PROB_1:28;

Lm2: for A holds 0 <= P.A
proof
  let A;
  now per cases;
    suppose 0 in A;
      then P.A = 1 by Lm1;
      hence thesis;
    end;
    suppose not 0 in A;
      hence thesis by Lm1;
    end;
  end;
  hence thesis;
end;

Lm3: P.REAL = 1
proof
  [#]REAL in Borel_Sets by PROB_1:5;
  hence thesis by Lm1;
end;

Lm4: for A,B st A misses B holds P.(A \/ B) = P.A + P.B
proof
  let A,B such that
A1: A misses B;
  now
    per cases by A1,XBOOLE_0:3;
    suppose
A2:   0 in A & not 0 in B; then
A3:   0 in A \/ B by XBOOLE_0:def 3;
      P.A = 1 & P.B = 0 by A2,Lm1;
      hence thesis by A3,Lm1;
    end;
    suppose
A4:   not 0 in A & 0 in B;
      then
A5:   0 in A \/ B by XBOOLE_0:def 3;
      P.A = 0 & P.B = 1 by A4,Lm1;
      hence thesis by A5,Lm1;
    end;
    suppose
A6:   not 0 in A & not 0 in B;
      then
A7:   not 0 in (A \/ B) by XBOOLE_0:def 3;
      P.A = 0 & P.B = 0 by A6,Lm1;
      hence thesis by A7,Lm1;
    end;
  end;
  hence thesis;
end;

for ASeq st ASeq is non-ascending holds P * ASeq is convergent & lim (P *
ASeq) = P.Intersection ASeq
proof
  let ASeq;
A1: now
    let n;
    dom (P * ASeq) = NAT by FUNCT_2:def 1;
    hence (P * ASeq).n = P.(ASeq.n) by FUNCT_1:12;
  end;
  assume
A2: ASeq is non-ascending;
  now
    per cases;
    suppose
A3:   for n holds 0 in ASeq.n;
      reconsider r = 1 as Real;
      rng ASeq c= Borel_Sets by RELAT_1:def 19;
      then
A4:   Intersection ASeq in Borel_Sets by PROB_1:def 6;
A5:   0 in Intersection ASeq by A3,PROB_1:13;
A6:   now
        let n;
A7:     rng ASeq c= Borel_Sets & ASeq.n in rng ASeq by NAT_1:51,RELAT_1:def 19;
        0 in ASeq.n by A3;
        then P.(ASeq.n) = 1 by A7,Lm1;
        hence (P * ASeq).n = 1 by A1;
      end;
A8:   ex m st for n st m <= n holds (P * ASeq).n = r
      proof
        take 0;
        thus thesis by A6;
      end;
      then lim (P * ASeq) = 1 by PROB_1:1;
      hence thesis by A8,A5,A4,Lm1,PROB_1:1;
    end;
    suppose
A9:   not (for n holds 0 in ASeq.n);
      rng ASeq c= Borel_Sets by RELAT_1:def 19;
      then
A10:  Intersection ASeq in Borel_Sets by PROB_1:def 6;
A11:  not 0 in Intersection ASeq by A9,PROB_1:13;
A12:  ex m st for n st m <= n holds (P * ASeq).n = 0
      proof
        consider m such that
A13:    not 0 in ASeq.m by A9;
        take m;
        for n st m <= n holds (P * ASeq).n = 0
        proof
          let n;
          assume m <= n;
          then ASeq.n c= ASeq.m by A2,PROB_1:def 4;
          then
A14:      not 0 in ASeq.n by A13;
          rng ASeq c= Borel_Sets & ASeq.n in rng ASeq by NAT_1:51
,RELAT_1:def 19;
          then P.(ASeq.n) = 0 by A14,Lm1;
          hence thesis by A1;
        end;
        hence thesis;
      end;
      then lim (P * ASeq) = 0 by PROB_1:1;
      hence thesis by A12,A11,A10,Lm1,PROB_1:1;
    end;
  end;
  hence thesis;
end;

then reconsider P as Probability of Borel_Sets by Lm2,Lm3,Lm4,PROB_1:def 8;
set f = { [ [0,0], P] };
dom f = { [0,0] } by RELAT_1:9;
then

Lm5: dom f = [:X,X:] by ZFMISC_1:29;

rng f = {P} & P in Probabilities(Borel_Sets) by Def1,RELAT_1:9;

then rng f c= Probabilities(Borel_Sets) by ZFMISC_1:31;

then reconsider
Y = f as Function of [:X, X:], Probabilities(Borel_Sets) by Lm5,FUNCT_2:def 1
,RELSET_1:4;

Lm6: now
  thus for A1,A2 being Element of Obs QM_Str(#X,X,Y#) st for s being Element
  of Sts QM_Str(#X,X,Y#) holds Meas(A1,s)=Meas(A2,s) holds A1=A2
  proof
    let A1,A2 be Element of Obs QM_Str(#X,X,Y#);
    A1=0 by TARSKI:def 1;
    hence thesis by TARSKI:def 1;
  end;
  thus for s1,s2 being Element of Sts QM_Str(#X,X,Y#) st for A being Element
  of Obs QM_Str(#X,X,Y#) holds Meas(A,s1)=Meas(A,s2) holds s1=s2
  proof
    let s1,s2 be Element of Sts QM_Str(#X,X,Y#);
    s1=0 by TARSKI:def 1;
    hence thesis by TARSKI:def 1;
  end;
  thus for s1,s2 being Element of Sts QM_Str(#X,X,Y#), t being Real st 0<=t &
  t<=1 ex s being Element of Sts QM_Str(#X,X,Y#) st for A being Element of Obs
  QM_Str(#X,X,Y#), E holds Meas(A,s).E=t*(Meas(A,s1).E) + ((1-t)*Meas(A,s2).E)
  proof
    let s1,s2 be Element of Sts QM_Str(#X,X,Y#);
    let t be Real;
    assume 0<=t & t<=1;
    take s2;
    let A be Element of Obs QM_Str(#X,X,Y#), E;
    s1=0 & s2=0 by TARSKI:def 1;
    hence thesis;
  end;
end;

definition let IT be QM_Str;
  attr IT is Quantum_Mechanics-like means
  :Def5:
  (for A1,A2 being Element of Obs IT st
  for s being Element of Sts IT holds Meas(A1,s)=Meas(A2,s) holds A1=A2) &
  (for s1,s2 being Element of Sts IT st for A being Element of Obs IT holds
  Meas(A,s1)=Meas(A,s2) holds s1=s2) &
  for s1,s2 being Element of Sts IT, t being Real st 0<=t & t<=1
  ex s being Element of Sts IT st for A being Element of Obs IT, E holds
  Meas(A,s).E=t*(Meas(A,s1).E) + ((1-t)*Meas(A,s2).E);
end;

registration
  cluster strict Quantum_Mechanics-like for QM_Str;
  existence
  proof
    QM_Str(#X,X,Y#) is Quantum_Mechanics-like by Def5,Lm6;
    hence thesis;
  end;
end;

definition
  mode Quantum_Mechanics is Quantum_Mechanics-like QM_Str;
end;

reserve Q for Quantum_Mechanics;
reserve s for Element of Sts Q;

definition
  struct(RelStr,ComplStr) OrthoRelStr(# carrier -> set,
  InternalRel -> (Relation of the carrier),
  Compl -> Function of the carrier,the carrier #);
end;

reserve x1 for Element of X1;
reserve Inv for Function of X1,X1;

definition let X1, Inv;
  pred Inv is_an_involution means
  Inv.(Inv.x1) = x1;
end;

definition let W be OrthoRelStr;
  pred W is_a_Quantum_Logic means
  :Def7:
  the InternalRel of W partially_orders the carrier of W &
  the Compl of W is_an_involution &
  for x,y being Element of W st
  [x,y] in the InternalRel of W holds
  [(the Compl of W).y,(the Compl of W).x] in the InternalRel of W;
end;

definition let Q;
  func Prop Q -> set equals
  [:Obs Q,Borel_Sets:];
  coherence;
end;

registration let Q;
  cluster Prop Q -> non empty;
  coherence;
end;

reserve p,q,r,p1,q1 for Element of Prop Q;

definition let Q,p;
  redefine func p`1 -> Element of Obs Q;
  coherence by MCART_1:10;
  redefine func p`2 -> Event of Borel_Sets;
  coherence by MCART_1:10;
end;

theorem Th1:
  for E st E = p`2` holds Meas(p`1,s).p`2 = 1 - Meas(p`1,s).E
proof
  let E such that
A1: E = p`2`;
  [#] Borel_Sets = REAL & REAL \ E = E` by PROB_1:def 7;
  hence thesis by A1,PROB_1:32;
end;

definition let Q,p;
  func 'not' p -> Element of Prop Q equals
  [p`1,(p`2)`];
  coherence
  proof
    reconsider x = p`2` as Event of Borel_Sets by PROB_1:20;
    x in Borel_Sets;
    hence thesis by ZFMISC_1:87;
  end;
  involutiveness
  proof
    let r,p be Element of Prop Q;
    assume
A1: r = [p`1,(p`2)`];
    thus p = [p`1,((p`2)`)`] by MCART_1:21
    .= [r`1,((p`2)`)`] by A1,MCART_1:7
    .= [r`1,(r`2)`] by A1,MCART_1:7;
  end;
end;

definition let Q,p,q;
  pred p |- q means
  :Def10:
  for s holds Meas(p`1,s).p`2 <= Meas(q`1,s).q`2;
  reflexivity;
end;

definition let Q,p,q;
  pred p <==> q means
  :Def11:
  p |- q & q |- p;
  reflexivity;
  symmetry;
end;

theorem Th2:
  p <==> q iff for s holds Meas(p`1,s).p`2 = Meas(q`1,s).q`2
proof
  thus p <==> q implies for s holds Meas(p`1,s).p`2 = Meas(q`1,s).q`2
  proof
    assume
A1: p <==> q;
    let s;
    q |- p by A1,Def11; then
A2: Meas(q`1,s).q`2 <= Meas(p`1,s).p`2 by Def10;
    p |- q by A1,Def11;
    then Meas(p`1,s).p`2 <= Meas(q`1,s).q`2 by Def10;
    hence thesis by A2,XXREAL_0:1;
  end;
  assume
A3: for s holds Meas(p`1,s).p`2 = Meas(q`1,s).q`2;
  thus p |- q
  proof
    let s;
    thus thesis by A3;
  end;
  let s;
  thus thesis by A3;
end;

theorem
  p |- p;

theorem Th4:
  p |- q & q |- r implies p |- r
proof
  assume
A1: p |- q & q |- r;
  let s;
  Meas(p`1,s).p`2 <= Meas(q`1,s).q`2 & Meas(q`1,s).q`2 <= Meas(r`1,s).r`2
  by A1,Def10;
  hence thesis by XXREAL_0:2;
end;

theorem
  p <==> p;

theorem
  p <==> q implies q <==> p;

theorem Th7:
  p <==> q & q <==> r implies p <==> r
proof
  assume p |- q & q |- p & q |- r & r |- q;
  hence p |- r & r |- p by Th4;
end;

canceled;

theorem Th9:
  p |- q implies 'not' q |- 'not' p
proof
  assume
A1: p |- q;
  let s;
  reconsider E1 = q`2` as Event of Borel_Sets by PROB_1:20;
  reconsider E = p`2` as Event of Borel_Sets by PROB_1:20;
  set p1 = Meas(p`1,s).E, p2 = Meas(q`1,s).E1;
A2: -(1-p1) = p1 -1 & -(1-p2) = p2 -1;
A3: ('not' p)`1 = p`1 & ('not' p)`2 = (p`2)` by MCART_1:7;
A4: Meas(q`1,s).q`2 = 1 - p2 & Meas(p`1,s).p`2 = 1 - p1 by Th1;
A5: ('not' q)`1 = q`1 & ('not' q)`2 = (q`2)` by MCART_1:7;
  Meas(p`1,s).p`2 <= Meas(q`1,s).q`2 by A1,Def10;
  then p2 -1 <= p1 - 1 by A4,A2,XREAL_1:24;
  hence thesis by A5,A3,XREAL_1:9;
end;

definition let Q;
  func PropRel Q -> Equivalence_Relation of Prop Q means
  :Def12:
  [p,q] in it iff p <==> q;
  existence
  proof
    defpred P[set,set] means ex p,q st p=$1 & q = $2 & p <==> q;
A1: for x,y st P[x,y] holds P[y,x];
A2: for x,y,z st P[x,y] & P[y,z] holds P[x,z] by Th7;
A3: for x st x in Prop Q holds P[x,x];
    consider R being Equivalence_Relation of Prop Q such that
A4: for x,y holds [x,y] in R iff x in Prop Q & y in Prop Q & P[x,y]
    from EQREL_1:sch 1(A3,A1,A2);
    take R;
    [p,q] in R iff p <==> q
    proof
      thus [p,q] in R implies p <==> q
      proof
        assume [p,q] in R;
        then ex p1,q1 st p1=p & q1=q & p1 <==> q1 by A4;
        hence thesis;
      end;
      assume p <==> q;
      hence thesis by A4;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let R1,R2 be Equivalence_Relation of Prop Q;
    assume that
A5: for p,q holds [p,q] in R1 iff p <==> q and
A6: for p,q holds [p,q] in R2 iff p <==> q;
A7: now
      let p,q;
      [p,q] in R1 iff p <==> q by A5;
      hence [p,q] in R1 iff [p,q] in R2 by A6;
    end;
    for x,y holds [x,y] in R1 iff [x,y] in R2
    proof
      let x,y;
      thus [x,y] in R1 implies [x,y] in R2
      proof
        assume
A8:     [x,y] in R1;
        then x is Element of Prop Q & y is Element of Prop Q by ZFMISC_1:87;
        hence thesis by A7,A8;
      end;
      assume
A9:   [x,y] in R2;
      then x is Element of Prop Q & y is Element of Prop Q by ZFMISC_1:87;
      hence thesis by A7,A9;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

reserve B,C for Subset of Prop Q;

theorem Th10:
  for B,C st B in Class PropRel Q & C in Class PropRel Q for a,b,c
  ,d being Element of Prop Q holds a in B & b in B & c in C & d in C & a |- c
  implies b |- d
proof
  let B,C such that
A1: B in Class PropRel Q and
A2: C in Class PropRel Q;
  let a,b,c,d be Element of Prop Q;
  assume that
A3: a in B & b in B and
A4: c in C & d in C;
  assume
A5: a |- c;
  let s;
  ex y st y in Prop Q & C = Class(PropRel Q,y) by A2,EQREL_1:def 3;
  then [c,d] in PropRel Q by A4,EQREL_1:22;
  then c <==> d by Def12;
  then
A6: Meas(c`1,s).c`2 = Meas(d`1,s).d`2 by Th2;
  ex x st x in Prop Q & B = Class(PropRel Q,x) by A1,EQREL_1:def 3;
  then [a,b] in PropRel Q by A3,EQREL_1:22;
  then a <==> b by Def12;
  then Meas(a`1,s).a`2 = Meas(b`1,s).b`2 by Th2;
  hence thesis by A5,A6,Def10;
end;

definition let Q;
  func OrdRel Q -> Relation of Class PropRel (Q) means
  :Def13:
  [B,C] in it iff B in Class PropRel Q & C in Class PropRel Q &
  for p,q st p in B & q in C holds p |- q;
  existence
  proof
    defpred P[set,set] means ex B,C st $1 = B & $2 = C & for p,q st p in B & q
    in C holds p |- q;
    consider R being Relation of Class PropRel Q,Class PropRel Q such that
A1: for x,y holds [x,y] in R iff x in Class PropRel Q & y in Class
    PropRel Q & P[x,y] from RELSET_1:sch 1;
    [B,C] in R iff B in Class PropRel Q & C in Class PropRel Q & for p,q
    st p in B & q in C holds p |- q
    proof
      thus [B,C] in R implies B in Class PropRel Q & C in Class PropRel Q &
      for p,q st p in B & q in C holds p |- q
      proof
        assume
A2:     [B,C] in R; then
        ex B9,C9 being Subset of Prop Q st B = B9 & C = C9 & for p,q st p
        in B9 & q in C9 holds p |- q by A1;
        hence thesis by A1,A2;
      end;
      assume B in Class PropRel Q & C in Class PropRel Q & for p,q st p in B
      & q in C holds p |- q;
      hence thesis by A1;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let R1,R2 be Relation of Class PropRel Q;
    assume that
A3: for B,C holds [B,C] in R1 iff B in Class PropRel Q & C in Class
    PropRel Q & for p,q st p in B & q in C holds p |- q and
A4: for B,C holds [B,C] in R2 iff B in Class PropRel Q & C in Class
    PropRel Q & for p,q st p in B & q in C holds p |- q;
A5: now
      let B,C;
      [B,C] in R1 iff B in Class PropRel Q & C in Class PropRel Q & for p
      ,q st p in B & q in C holds p |- q by A3;
      hence [B,C] in R1 iff [B,C] in R2 by A4;
    end;
    for x,y holds [x,y] in R1 iff [x,y] in R2
    proof
      let x,y;
      thus [x,y] in R1 implies [x,y] in R2
      proof
        assume
A6:     [x,y] in R1;
        then x in Class PropRel Q & y in Class PropRel Q by ZFMISC_1:87;
        hence thesis by A5,A6;
      end;
      assume
A7:   [x,y] in R2;
      then x in Class PropRel Q & y in Class PropRel Q by ZFMISC_1:87;
      hence thesis by A5,A7;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

theorem Th11:
  p |- q iff [Class(PropRel Q,p),Class(PropRel Q,q)] in OrdRel Q
proof
  [p,p] in PropRel Q by Def12;
  then
A1: p in Class(PropRel Q,p) by EQREL_1:19;
  [q,q] in PropRel Q by Def12;
  then
A2: q in Class(PropRel Q,q) by EQREL_1:19;
A3: Class(PropRel Q,p) in Class PropRel Q & Class(PropRel Q,q) in Class
  PropRel Q by EQREL_1:def 3;
  thus p |- q implies [Class(PropRel Q,p),Class(PropRel Q,q)] in OrdRel Q
  proof
    assume p |- q;
    then for p1,q1 holds p1 in Class(PropRel Q,p) & q1 in Class(PropRel Q,q)
    implies p1 |- q1 by A1,A2,A3,Th10;
    hence thesis by A3,Def13;
  end;
  thus thesis by A1,A2,Def13;
end;

theorem Th12:
  for B,C st B in Class PropRel Q & C in Class PropRel Q for p1,q1
  holds p1 in B & q1 in B & 'not' p1 in C implies 'not' q1 in C
proof
  let B,C such that
A1: B in Class PropRel Q and
A2: C in Class PropRel Q;
  consider y such that
A3: y in Prop Q and
A4: C = Class(PropRel Q,y) by A2,EQREL_1:def 3;
  let p1,q1;
  assume that
A5: p1 in B & q1 in B and
A6: 'not' p1 in C;
  ex x st x in Prop Q & B = Class(PropRel Q,x) by A1,EQREL_1:def 3;
  then [p1,q1] in PropRel Q by A5,EQREL_1:22;
  then
A7: p1 <==> q1 by Def12;
  now
    reconsider E1 = q1`2`, E = p1`2` as Event of Borel_Sets
    by PROB_1:20;
    let s;
    set r1 = Meas(p1`1,s).E, r2 = Meas(q1`1,s).E1;
A8: ('not' p1)`1 = p1`1 & ('not' p1)`2 = (p1`2)` by MCART_1:7;
A9: ('not' q1)`1 = q1`1 by MCART_1:7;
    1 - r1 = Meas(p1`1,s).p1`2 by Th1
      .= Meas(q1`1,s).q1`2 by A7,Th2
      .= 1 - r2 by Th1;
    hence
    Meas(('not' p1)`1,s).('not' p1)`2 = Meas(('not' q1)`1,s).('not' q1)`2
    by A8,A9,MCART_1:7;
  end;
  then
A10: 'not' p1 <==> 'not' q1 by Th2;
  reconsider q = y as Element of Prop Q by A3;
  ['not' p1,q] in PropRel Q by A4,A6,EQREL_1:19;
  then 'not' p1 <==> q by Def12;
  then q <==> 'not' q1 by A10,Th7;
  then ['not' q1,q] in PropRel Q by Def12;
  hence thesis by A4,EQREL_1:19;
end;

theorem
  for B,C st B in Class PropRel Q & C in Class PropRel Q for p,q holds
  'not' p in C & 'not' q in C & p in B implies q in B
proof
  let B,C such that
A1: B in Class PropRel Q & C in Class PropRel Q;
  let p,q;
  'not'('not' p) = p & 'not'('not' q) =q;
  hence thesis by A1,Th12;
end;

definition let Q;
  func InvRel Q -> Function of Class PropRel Q,Class PropRel Q means
  :Def14:
  it.Class(PropRel Q,p) = Class(PropRel Q,'not' p);
  existence
  proof
    defpred P[set,set] means for p st $1 = Class(PropRel Q,p) holds $2 = Class
    (PropRel Q,'not' p);
A1: for x st x in Class PropRel Q ex y st y in Class PropRel Q & P[x,y]
    proof
      let x;
      assume
A2:   x in Class PropRel Q;
      then consider q such that
A3:   x = Class(PropRel Q,q) by EQREL_1:36;
      reconsider y = Class(PropRel Q,'not' q) as set;
      take y;
      thus
A4:   y in Class PropRel Q by EQREL_1:def 3;
      let p;
      assume
A5:   x = Class(PropRel Q,p);
      then reconsider x as Subset of Prop Q;
A6:   q in x by A3,EQREL_1:20;
      reconsider y9=y as Subset of Prop Q;
A7:   'not' q in y9 by EQREL_1:20;
      p in x by A5,EQREL_1:20;
      then 'not' p in y9 by A2,A4,A6,A7,Th12;
      hence thesis by EQREL_1:23;
    end;
    consider F being Function of Class PropRel Q,Class PropRel Q such that
A8: for x st x in Class PropRel Q holds P[x,F.x] from FUNCT_2:sch 1(
    A1);
    take F;
    let p;
    Class(PropRel Q,p) in Class PropRel Q by EQREL_1:def 3;
    hence thesis by A8;
  end;
  uniqueness
  proof
    let F1,F2 be Function of Class PropRel Q,Class PropRel Q;
    assume that
A9: for p holds F1.Class(PropRel Q,p) = Class(PropRel Q,'not' p) and
A10: for p holds F2.Class(PropRel Q,p) = Class(PropRel Q,'not' p);
    now let x;
      assume x in Class PropRel Q;
      then consider p such that
A11:  x = Class(PropRel Q, p) by EQREL_1:36;
      F1.x = Class(PropRel Q,'not' p) by A9,A11;
      hence F1.x = F2.x by A10,A11;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem :: Main Theorem
  for Q holds OrthoRelStr(#Class PropRel Q,OrdRel Q,InvRel Q#)
  is_a_Quantum_Logic
proof
  let Q;
A1: OrdRel Q is_transitive_in Class PropRel Q
  proof
    let x,y,z;
    assume that
A2: x in Class PropRel Q and
A3: y in Class PropRel Q and
A4: z in Class PropRel Q and
A5: [x,y] in OrdRel Q & [y,z] in OrdRel Q;
    consider p such that
A6: x = Class(PropRel Q,p) by A2,EQREL_1:36;
    consider r such that
A7: z = Class(PropRel Q,r) by A4,EQREL_1:36;
    consider q such that
A8: y = Class(PropRel Q,q) by A3,EQREL_1:36;
    p |- q & q |- r implies p |- r by Th4;
    hence thesis by A5,A6,A8,A7,Th11;
  end;
A9: OrdRel Q is_antisymmetric_in Class PropRel Q
  proof
    let x,y;
    assume that
A10: x in Class PropRel Q and
A11: y in Class PropRel Q and
A12: [x,y] in OrdRel Q & [y,x] in OrdRel Q;
    consider p such that
A13: x = Class(PropRel Q,p) by A10,EQREL_1:36;
    consider q such that
A14: y = Class(PropRel Q,q) by A11,EQREL_1:36;
A15: p <==> q implies [p,q] in PropRel Q by Def12;
    p |- q & q |- p implies p <==> q by Def11;
    hence thesis by A12,A13,A14,A15,Th11,EQREL_1:35;
  end;
A16: for x,y being Element of Class PropRel Q st [x,y] in OrdRel Q holds
  [(InvRel Q).y,(InvRel Q).x] in OrdRel Q
  proof

    let x,y be Element of Class PropRel Q;
    consider p such that
A17: x = Class(PropRel Q,p) by EQREL_1:36;
    consider q such that
A18: y = Class(PropRel Q,q) by EQREL_1:36;
A19: p |- q implies 'not' q |- 'not' p by Th9;
    (InvRel Q).Class(PropRel Q,p) = Class(PropRel Q,'not' p) & (InvRel Q)
    .Class( PropRel Q,q) = Class(PropRel Q,'not' q) by Def14;
    hence thesis by A17,A18,A19,Th11;
  end;
A20: InvRel Q is_an_involution
  proof

    let x be Element of Class PropRel Q;
    consider p such that
A21: x = Class(PropRel Q,p) by EQREL_1:36;
    (InvRel Q).((InvRel Q).x) = (InvRel Q).Class(PropRel Q,'not' p) by A21
,Def14
      .= Class(PropRel Q,'not'('not' p)) by Def14;
    hence thesis by A21;
  end;
  OrdRel Q is_reflexive_in Class PropRel Q
  proof
    let x;
    assume x in Class PropRel Q;
    then ex p st x = Class(PropRel Q,p) by EQREL_1:36;
    hence thesis by Th11;
  end;
  then OrdRel Q partially_orders Class PropRel Q by A1,A9,ORDERS_1:def 7;
  hence thesis by A20,A16,Def7;
end;