:: HILBERT1 semantic presentation

begin

definition
let D be set ;
attrD is with_VERUM  means :Def1: :: HILBERT1:def 1
<*0*> in D;
end;

:: deftheorem Def1 defines with_VERUM HILBERT1:def_1_:_
 for D being set holds
( D is with_VERUM iff <*0*> in D );

definition
let D be set ;
attrD is with_implication  means :Def2: :: HILBERT1:def 2
 for p, q being FinSequence st p in D & q in D holds
(<*1*> ^ p) ^ q in D;
end;

:: deftheorem Def2 defines with_implication HILBERT1:def_2_:_
 for D being set holds
( D is with_implication iff for p, q being FinSequence st p in D & q in D holds
(<*1*> ^ p) ^ q in D );

definition
let D be set ;
attrD is with_conjunction  means :Def3: :: HILBERT1:def 3
 for p, q being FinSequence st p in D & q in D holds
(<*2*> ^ p) ^ q in D;
end;

:: deftheorem Def3 defines with_conjunction HILBERT1:def_3_:_
 for D being set holds
( D is with_conjunction iff for p, q being FinSequence st p in D & q in D holds
(<*2*> ^ p) ^ q in D );

definition
let D be set ;
attrD is with_propositional_variables  means :Def4: :: HILBERT1:def 4
 for n being Element of NAT holds <*(3 + n)*> in D;
end;

:: deftheorem Def4 defines with_propositional_variables HILBERT1:def_4_:_
 for D being set holds
( D is with_propositional_variables iff for n being Element of NAT holds <*(3 + n)*> in D );

definition
let D be set ;
attrD is HP-closed  means :Def5: :: HILBERT1:def 5
( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables );
end;

:: deftheorem Def5 defines HP-closed HILBERT1:def_5_:_
 for D being set holds
( D is HP-closed iff ( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables ) );

Lm1:  for D being set st D is HP-closed holds
not D is empty
proof
let D be set ; ::_thesis: ( D is HP-closed implies not D is empty )
assume  D is HP-closed ; ::_thesis: not D is empty
then  D is with_VERUM by Def5;
hence  not D is empty by Def1; ::_thesis: verum
end;

registration
cluster HP-closed  ->  non empty with_VERUM with_implication with_conjunction with_propositional_variables for set ;
coherence
 for b1 being set st b1 is HP-closed holds
( b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables & not b1 is empty ) by Def5, Lm1;
cluster with_VERUM with_implication with_conjunction with_propositional_variables  ->  HP-closed for Element of K6((NAT *));
coherence
 for b1 being Subset of (NAT *) st b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables holds
b1 is HP-closed by Def5;
end;

definition
func HP-WFF  ->  set  means :Def6: :: HILBERT1:def 6
( it is HP-closed & ( for D being set st D is HP-closed holds
it c= D ) );
existence
 ex b1 being set st
( b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) )
proof
A1: <*0*> in NAT * by FINSEQ_1:def_11;
defpred S1[ set ] means  for D being set st D is HP-closed holds
$1 in D;
consider D0 being set  such that
A2: for x being set holds
( x in D0 iff ( x in NAT * & S1[x] ) ) from XBOOLE_0:sch_1();
A3: for D being set st D is HP-closed holds
<*0*> in D by Def1;
then reconsider D0 = D0 as non empty set by A2, A1;
take  D0 ; ::_thesis: ( D0 is HP-closed & ( for D being set st D is HP-closed holds
D0 c= D ) )
A4: D0 c= NAT *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in NAT * )
thus  ( not x in D0 or x in NAT * ) by A2; ::_thesis: verum
end;
 for p, q being FinSequence st p in D0 & q in D0 holds
(<*2*> ^ p) ^ q in D0
proof
let p, q be FinSequence; ::_thesis: ( p in D0 & q in D0 implies (<*2*> ^ p) ^ q in D0 )
assume that
A5: p in D0 and
A6: q in D0 ; ::_thesis: (<*2*> ^ p) ^ q in D0
A7: q in NAT * by A2, A6;
A8: for D being set st D is HP-closed holds
(<*2*> ^ p) ^ q in D
proof
let D be set ; ::_thesis: ( D is HP-closed implies (<*2*> ^ p) ^ q in D )
assume A9: D is HP-closed ; ::_thesis: (<*2*> ^ p) ^ q in D
then A10: q in D by A2, A6;
 p in D by A2, A5, A9;
hence  (<*2*> ^ p) ^ q in D by A9, A10, Def3; ::_thesis: verum
end;
 p in NAT * by A2, A5;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A7, FINSEQ_1:def_11;
 (<*2*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence  (<*2*> ^ p) ^ q in D0 by A2, A8; ::_thesis: verum
end;
then A11: D0 is with_conjunction by Def3;
 for p, q being FinSequence st p in D0 & q in D0 holds
(<*1*> ^ p) ^ q in D0
proof
let p, q be FinSequence; ::_thesis: ( p in D0 & q in D0 implies (<*1*> ^ p) ^ q in D0 )
assume that
A12: p in D0 and
A13: q in D0 ; ::_thesis: (<*1*> ^ p) ^ q in D0
A14: q in NAT * by A2, A13;
A15: for D being set st D is HP-closed holds
(<*1*> ^ p) ^ q in D
proof
let D be set ; ::_thesis: ( D is HP-closed implies (<*1*> ^ p) ^ q in D )
assume A16: D is HP-closed ; ::_thesis: (<*1*> ^ p) ^ q in D
then A17: q in D by A2, A13;
 p in D by A2, A12, A16;
hence  (<*1*> ^ p) ^ q in D by A16, A17, Def2; ::_thesis: verum
end;
 p in NAT * by A2, A12;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A14, FINSEQ_1:def_11;
 (<*1*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence  (<*1*> ^ p) ^ q in D0 by A2, A15; ::_thesis: verum
end;
then A18: D0 is with_implication by Def2;
 for n being Element of NAT holds <*(3 + n)*> in D0
proof
let n be Element of NAT ; ::_thesis: <*(3 + n)*> in D0
set p = 3 + n;
reconsider h = <*(3 + n)*> as FinSequence of NAT ;
A19: h in NAT * by FINSEQ_1:def_11;
 for D being set st D is HP-closed holds
<*(3 + n)*> in D by Def4;
hence  <*(3 + n)*> in D0 by A2, A19; ::_thesis: verum
end;
then A20: D0 is with_propositional_variables by Def4;
 <*0*> in D0 by A2, A1, A3;
then  D0 is with_VERUM by Def1;
hence  D0 is HP-closed by A4, A20, A18, A11; ::_thesis: for D being set st D is HP-closed holds
D0 c= D
let D be set ; ::_thesis: ( D is HP-closed implies D0 c= D )
assume A21: D is HP-closed ; ::_thesis: D0 c= D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in D )
assume  x in D0 ; ::_thesis: x in D
hence  x in D by A2, A21; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) & b2 is HP-closed & ( for D being set st D is HP-closed holds
b2 c= D ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( D1 is HP-closed & ( for D being set st D is HP-closed holds
D1 c= D ) & D2 is HP-closed & ( for D being set st D is HP-closed holds
D2 c= D ) implies D1 = D2 )
assume that
A22: D1 is HP-closed and
A23: for D being set st D is HP-closed holds
D1 c= D and
A24: D2 is HP-closed and
A25: for D being set st D is HP-closed holds
D2 c= D ; ::_thesis: D1 = D2
A26: D2 c= D1 by A22, A25;
 D1 c= D2 by A23, A24;
hence  D1 = D2 by A26, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines HP-WFF HILBERT1:def_6_:_
 for b1 being set holds
( b1 = HP-WFF iff ( b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) ) );

registration
cluster HP-WFF  ->  HP-closed ;
coherence
 HP-WFF is HP-closed by Def6;
end;

registration
cluster non empty HP-closed for set ;
existence
 ex b1 being set st
( b1 is HP-closed & not b1 is empty )
proof
take  HP-WFF ; ::_thesis: ( HP-WFF is HP-closed & not HP-WFF is empty )
thus  ( HP-WFF is HP-closed & not HP-WFF is empty ) ; ::_thesis: verum
end;
end;

registration
cluster HP-WFF  ->  functional ;
coherence
 HP-WFF is functional
proof
 HP-WFF c= NAT * by Def5;
hence  HP-WFF is functional ; ::_thesis: verum
end;
end;

registration
cluster  ->  FinSequence-like for Element of HP-WFF ;
coherence
 for b1 being Element of HP-WFF holds b1 is FinSequence-like
proof
let p be Element of HP-WFF ; ::_thesis: p is FinSequence-like
 HP-WFF c= NAT * by Def5;
hence  p is FinSequence-like ; ::_thesis: verum
end;
end;

definition
mode HP-formula is Element of HP-WFF ;
end;

definition
func VERUM  ->  HP-formula equals :: HILBERT1:def 7
<*0*>;
correctness
coherence
<*0*> is HP-formula;
by Def1;
let p, q be Element of HP-WFF ;
funcp => q ->  HP-formula equals :: HILBERT1:def 8
(<*1*> ^ p) ^ q;
coherence
 (<*1*> ^ p) ^ q is HP-formula by Def2;
funcp '&' q ->  HP-formula equals :: HILBERT1:def 9
(<*2*> ^ p) ^ q;
correctness
coherence
(<*2*> ^ p) ^ q is HP-formula;
by Def3;
end;

:: deftheorem  defines VERUM HILBERT1:def_7_:_
 VERUM = <*0*>;

:: deftheorem  defines => HILBERT1:def_8_:_
 for p, q being Element of HP-WFF holds p => q = (<*1*> ^ p) ^ q;

:: deftheorem  defines '&' HILBERT1:def_9_:_
 for p, q being Element of HP-WFF holds p '&' q = (<*2*> ^ p) ^ q;


definition
let T be Subset of HP-WFF;
attrT is Hilbert_theory  means :Def10: :: HILBERT1:def 10
( VERUM in T & ( for p, q, r being Element of HP-WFF holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & ( p in T & p => q in T implies q in T ) ) ) );
correctness
;
end;

:: deftheorem Def10 defines Hilbert_theory HILBERT1:def_10_:_
 for T being Subset of HP-WFF holds
( T is Hilbert_theory iff ( VERUM in T & ( for p, q, r being Element of HP-WFF holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & ( p in T & p => q in T implies q in T ) ) ) ) );

definition
let X be Subset of HP-WFF;
func CnPos X ->  Subset of HP-WFF means :Def11: :: HILBERT1:def 11
 for r being Element of HP-WFF holds
( r in it iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T );
existence
 ex b1 being Subset of HP-WFF st
for r being Element of HP-WFF holds
( r in b1 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T )
proof
defpred S1[ set ] means  for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
$1 in T;
consider Y being set  such that
A1: for a being set holds
( a in Y iff ( a in HP-WFF & S1[a] ) ) from XBOOLE_0:sch_1();
 Y c= HP-WFF
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in HP-WFF )
assume  a in Y ; ::_thesis: a in HP-WFF
hence  a in HP-WFF by A1; ::_thesis: verum
end;
then reconsider Z = Y as Subset of HP-WFF ;
take  Z ; ::_thesis: for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T )
thus  for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of HP-WFF st ( for r being Element of HP-WFF holds
( r in b1 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) & ( for r being Element of HP-WFF holds
( r in b2 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof
let Y, Z be Subset of HP-WFF; ::_thesis: ( ( for r being Element of HP-WFF holds
( r in Y iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) & ( for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of HP-WFF holds
( r in Y iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) and
A3: for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ; ::_thesis: Y = Z
 for a being set holds
( a in Y iff a in Z )
proof
let a be set ; ::_thesis: ( a in Y iff a in Z )
hereby  ::_thesis: ( a in Z implies a in Y )
assume A4: a in Y ; ::_thesis: a in Z
then reconsider t = a as Element of HP-WFF ;
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T by A2, A4;
hence  a in Z by A3; ::_thesis: verum
end;
assume A5: a in Z ; ::_thesis: a in Y
then reconsider t = a as Element of HP-WFF ;
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T by A3, A5;
hence  a in Y by A2; ::_thesis: verum
end;
hence  Y = Z by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines CnPos HILBERT1:def_11_:_
 for X, b2 being Subset of HP-WFF holds
( b2 = CnPos X iff for r being Element of HP-WFF holds
( r in b2 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) );

definition
func HP_TAUT  ->  Subset of HP-WFF equals :: HILBERT1:def 12
 CnPos ({} HP-WFF);
correctness
coherence
CnPos ({} HP-WFF) is Subset of HP-WFF;
;
end;

:: deftheorem  defines HP_TAUT HILBERT1:def_12_:_
 HP_TAUT = CnPos ({} HP-WFF);

theorem Th1: :: HILBERT1:1
for X being Subset of HP-WFF holds VERUM in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: VERUM in CnPos X
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
VERUM in T by Def10;
hence  VERUM in CnPos X by Def11; ::_thesis: verum
end;

theorem Th2: :: HILBERT1:2
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: p => (q => (p '&' q)) in CnPos X
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
p => (q => (p '&' q)) in T by Def10;
hence  p => (q => (p '&' q)) in CnPos X by Def11; ::_thesis: verum
end;

theorem Th3: :: HILBERT1:3
for X being Subset of HP-WFF
for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X
let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((p => q) => (p => r)) in CnPos X
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
(p => (q => r)) => ((p => q) => (p => r)) in T by Def10;
hence  (p => (q => r)) => ((p => q) => (p => r)) in CnPos X by Def11; ::_thesis: verum
end;

theorem Th4: :: HILBERT1:4
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds p => (q => p) in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds p => (q => p) in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: p => (q => p) in CnPos X
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
p => (q => p) in T by Def10;
hence  p => (q => p) in CnPos X by Def11; ::_thesis: verum
end;

theorem Th5: :: HILBERT1:5
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => p in CnPos X
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
(p '&' q) => p in T by Def10;
hence  (p '&' q) => p in CnPos X by Def11; ::_thesis: verum
end;

theorem Th6: :: HILBERT1:6
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds (p '&' q) => q in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds (p '&' q) => q in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => q in CnPos X
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
(p '&' q) => q in T by Def10;
hence  (p '&' q) => q in CnPos X by Def11; ::_thesis: verum
end;

theorem Th7: :: HILBERT1:7
for X being Subset of HP-WFF
for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds
q in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds
q in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: ( p in CnPos X & p => q in CnPos X implies q in CnPos X )
assume that
A1: p in CnPos X and
A2: p => q in CnPos X ; ::_thesis: q in CnPos X
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
q in T
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies q in T )
assume that
A3: T is Hilbert_theory and
A4: X c= T ; ::_thesis: q in T
A5: p => q in T by A2, A3, A4, Def11;
 p in T by A1, A3, A4, Def11;
hence  q in T by A3, A5, Def10; ::_thesis: verum
end;
hence  q in CnPos X by Def11; ::_thesis: verum
end;

theorem Th8: :: HILBERT1:8
for T, X being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
CnPos X c= T
proof
let T, X be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies CnPos X c= T )
assume that
A1: T is Hilbert_theory and
A2: X c= T ; ::_thesis: CnPos X c= T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos X or a in T )
thus  ( not a in CnPos X or a in T ) by A1, A2, Def11; ::_thesis: verum
end;

theorem Th9: :: HILBERT1:9
for X being Subset of HP-WFF holds X c= CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: X c= CnPos X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnPos X )
assume A1: a in X ; ::_thesis: a in CnPos X
then reconsider t = a as Element of HP-WFF ;
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T by A1;
hence  a in CnPos X by Def11; ::_thesis: verum
end;

theorem Th10: :: HILBERT1:10
for X, Y being Subset of HP-WFF st X c= Y holds
CnPos X c= CnPos Y
proof
let X, Y be Subset of HP-WFF; ::_thesis: ( X c= Y implies CnPos X c= CnPos Y )
assume A1: X c= Y ; ::_thesis: CnPos X c= CnPos Y
thus  CnPos X c= CnPos Y ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos X or a in CnPos Y )
assume A2: a in CnPos X ; ::_thesis: a in CnPos Y
then reconsider t = a as Element of HP-WFF ;
 for T being Subset of HP-WFF st T is Hilbert_theory & Y c= T holds
t in T
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & Y c= T implies t in T )
assume that
A3: T is Hilbert_theory and
A4: Y c= T ; ::_thesis: t in T
 X c= T by A1, A4, XBOOLE_1:1;
hence  t in T by A2, A3, Def11; ::_thesis: verum
end;
hence  a in CnPos Y by Def11; ::_thesis: verum
end;
end;

Lm2:  for X being Subset of HP-WFF holds CnPos (CnPos X) c= CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: CnPos (CnPos X) c= CnPos X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos (CnPos X) or a in CnPos X )
assume A1: a in CnPos (CnPos X) ; ::_thesis: a in CnPos X
then reconsider t = a as Element of HP-WFF ;
 for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies t in T )
assume that
A2: T is Hilbert_theory and
A3: X c= T ; ::_thesis: t in T
 CnPos X c= T by A2, A3, Th8;
hence  t in T by A1, A2, Def11; ::_thesis: verum
end;
hence  a in CnPos X by Def11; ::_thesis: verum
end;

theorem :: HILBERT1:11
for X being Subset of HP-WFF holds CnPos (CnPos X) = CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: CnPos (CnPos X) = CnPos X
A1: CnPos X c= CnPos (CnPos X) by Th9;
 CnPos (CnPos X) c= CnPos X by Lm2;
hence  CnPos (CnPos X) = CnPos X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm3:  for X being Subset of HP-WFF holds CnPos X is Hilbert_theory
proof
let X be Subset of HP-WFF; ::_thesis: CnPos X is Hilbert_theory
thus  VERUM in CnPos X by Th1; :: according to HILBERT1:def_10 ::_thesis: for p, q, r being Element of HP-WFF holds
( p => (q => p) in CnPos X & (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
let p, q, r be Element of HP-WFF ; ::_thesis: ( p => (q => p) in CnPos X & (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus  p => (q => p) in CnPos X by Th4; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus  (p => (q => r)) => ((p => q) => (p => r)) in CnPos X by Th3; ::_thesis: ( (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus  (p '&' q) => p in CnPos X by Th5; ::_thesis: ( (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus  (p '&' q) => q in CnPos X by Th6; ::_thesis: ( p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus  p => (q => (p '&' q)) in CnPos X by Th2; ::_thesis: ( p in CnPos X & p => q in CnPos X implies q in CnPos X )
thus  ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) by Th7; ::_thesis: verum
end;

registration
let X be Subset of HP-WFF;
cluster CnPos X ->  Hilbert_theory ;
coherence
 CnPos X is Hilbert_theory by Lm3;
end;

theorem Th12: :: HILBERT1:12
for T being Subset of HP-WFF holds
( T is Hilbert_theory iff CnPos T = T )
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory iff CnPos T = T )
hereby  ::_thesis: ( CnPos T = T implies T is Hilbert_theory )
assume A1: T is Hilbert_theory ; ::_thesis: CnPos T = T
A2: CnPos T c= T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos T or a in T )
assume  a in CnPos T ; ::_thesis: a in T
hence  a in T by A1, Def11; ::_thesis: verum
end;
 T c= CnPos T by Th9;
hence  CnPos T = T by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( CnPos T = T implies T is Hilbert_theory ) ; ::_thesis: verum
end;

theorem :: HILBERT1:13
for T being Subset of HP-WFF st T is Hilbert_theory holds
HP_TAUT c= T
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory implies HP_TAUT c= T )
assume A1: T is Hilbert_theory ; ::_thesis: HP_TAUT c= T
 HP_TAUT c= CnPos T by Th10, XBOOLE_1:2;
hence  HP_TAUT c= T by A1, Th12; ::_thesis: verum
end;

registration
cluster HP_TAUT  ->  Hilbert_theory ;
coherence
 HP_TAUT is Hilbert_theory ;
end;

begin

theorem Th14: :: HILBERT1:14
for p being Element of HP-WFF holds p => p in HP_TAUT
proof
let p be Element of HP-WFF ; ::_thesis: p => p in HP_TAUT
A1: p => (p => p) in HP_TAUT by Def10;
A2: p => ((p => p) => p) in HP_TAUT by Def10;
 (p => ((p => p) => p)) => ((p => (p => p)) => (p => p)) in HP_TAUT by Def10;
then  (p => (p => p)) => (p => p) in HP_TAUT by A2, Def10;
hence  p => p in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th15: :: HILBERT1:15
for q, p being Element of HP-WFF st q in HP_TAUT holds
p => q in HP_TAUT
proof
let q, p be Element of HP-WFF ; ::_thesis: ( q in HP_TAUT implies p => q in HP_TAUT )
 q => (p => q) in HP_TAUT by Def10;
hence  ( q in HP_TAUT implies p => q in HP_TAUT ) by Def10; ::_thesis: verum
end;

theorem :: HILBERT1:16
for p being Element of HP-WFF holds p => VERUM in HP_TAUT by Th1, Th15;

theorem :: HILBERT1:17
for p, q being Element of HP-WFF holds (p => q) => (p => p) in HP_TAUT by Th14, Th15;

theorem :: HILBERT1:18
for q, p being Element of HP-WFF holds (q => p) => (p => p) in HP_TAUT by Th14, Th15;

theorem Th19: :: HILBERT1:19
for q, r, p being Element of HP-WFF holds (q => r) => ((p => q) => (p => r)) in HP_TAUT
proof
let q, r, p be Element of HP-WFF ; ::_thesis: (q => r) => ((p => q) => (p => r)) in HP_TAUT
A1: (p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
A2: ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) => (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r)))) in HP_TAUT by Def10;
 ((p => (q => r)) => ((p => q) => (p => r))) => ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in HP_TAUT by Def10;
then  (q => r) => ((p => (q => r)) => ((p => q) => (p => r))) in HP_TAUT by A1, Def10;
then A3: ((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r))) in HP_TAUT by A2, Def10;
 (q => r) => (p => (q => r)) in HP_TAUT by Def10;
hence  (q => r) => ((p => q) => (p => r)) in HP_TAUT by A3, Def10; ::_thesis: verum
end;

theorem Th20: :: HILBERT1:20
for p, q, r being Element of HP-WFF st p => (q => r) in HP_TAUT holds
q => (p => r) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ( p => (q => r) in HP_TAUT implies q => (p => r) in HP_TAUT )
assume A1: p => (q => r) in HP_TAUT ; ::_thesis: q => (p => r) in HP_TAUT
A2: ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in HP_TAUT by Th19;
 (p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
then  (p => q) => (p => r) in HP_TAUT by A1, Def10;
then A3: (q => (p => q)) => (q => (p => r)) in HP_TAUT by A2, Def10;
 q => (p => q) in HP_TAUT by Def10;
hence  q => (p => r) in HP_TAUT by A3, Def10; ::_thesis: verum
end;

theorem Th21: :: HILBERT1:21
for p, q, r being Element of HP-WFF holds (p => q) => ((q => r) => (p => r)) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: (p => q) => ((q => r) => (p => r)) in HP_TAUT
 (q => r) => ((p => q) => (p => r)) in HP_TAUT by Th19;
hence  (p => q) => ((q => r) => (p => r)) in HP_TAUT by Th20; ::_thesis: verum
end;

theorem Th22: :: HILBERT1:22
for p, q, r being Element of HP-WFF st p => q in HP_TAUT holds
(q => r) => (p => r) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ( p => q in HP_TAUT implies (q => r) => (p => r) in HP_TAUT )
assume A1: p => q in HP_TAUT ; ::_thesis: (q => r) => (p => r) in HP_TAUT
 (p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21;
hence  (q => r) => (p => r) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th23: :: HILBERT1:23
for p, q, r being Element of HP-WFF st p => q in HP_TAUT & q => r in HP_TAUT holds
p => r in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ( p => q in HP_TAUT & q => r in HP_TAUT implies p => r in HP_TAUT )
assume that
A1: p => q in HP_TAUT and
A2: q => r in HP_TAUT ; ::_thesis: p => r in HP_TAUT
 (p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21;
then  (q => r) => (p => r) in HP_TAUT by A1, Def10;
hence  p => r in HP_TAUT by A2, Def10; ::_thesis: verum
end;

Lm4:  for q, r, p, s being Element of HP-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT
proof
let q, r, p, s be Element of HP-WFF ; ::_thesis: (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT
 (p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21;
hence  (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT by Th22; ::_thesis: verum
end;

theorem Th24: :: HILBERT1:24
for p, q, r, s being Element of HP-WFF holds (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT
proof
let p, q, r, s be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT
A1: (((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) in HP_TAUT by Lm4;
 ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r)))) in HP_TAUT by Lm4;
hence  (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem :: HILBERT1:25
for p, q, r being Element of HP-WFF holds ((p => q) => r) => (q => r) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ((p => q) => r) => (q => r) in HP_TAUT
A1: (q => (p => q)) => (((p => q) => r) => (q => r)) in HP_TAUT by Th21;
 q => (p => q) in HP_TAUT by Def10;
hence  ((p => q) => r) => (q => r) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th26: :: HILBERT1:26
for p, q, r being Element of HP-WFF holds (p => (q => r)) => (q => (p => r)) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => (q => (p => r)) in HP_TAUT
A1: q => (p => q) in HP_TAUT by Def10;
 (p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
then A2: (p => q) => ((p => (q => r)) => (p => r)) in HP_TAUT by Th20;
 ((p => q) => ((p => (q => r)) => (p => r))) => ((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in HP_TAUT by Th19;
then  (q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in HP_TAUT by A2, Def10;
then  q => ((p => (q => r)) => (p => r)) in HP_TAUT by A1, Def10;
hence  (p => (q => r)) => (q => (p => r)) in HP_TAUT by Th20; ::_thesis: verum
end;

theorem Th27: :: HILBERT1:27
for p, q being Element of HP-WFF holds (p => (p => q)) => (p => q) in HP_TAUT
proof
let p, q be Element of HP-WFF ; ::_thesis: (p => (p => q)) => (p => q) in HP_TAUT
 (p => (p => q)) => ((p => p) => (p => q)) in HP_TAUT by Def10;
then A1: (p => p) => ((p => (p => q)) => (p => q)) in HP_TAUT by Th20;
 p => p in HP_TAUT by Th14;
hence  (p => (p => q)) => (p => q) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem :: HILBERT1:28
for q, p being Element of HP-WFF holds q => ((q => p) => p) in HP_TAUT
proof
let q, p be Element of HP-WFF ; ::_thesis: q => ((q => p) => p) in HP_TAUT
A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in HP_TAUT by Th26;
 (q => p) => (q => p) in HP_TAUT by Th14;
hence  q => ((q => p) => p) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th29: :: HILBERT1:29
for s, q, p being Element of HP-WFF st s => (q => p) in HP_TAUT & q in HP_TAUT holds
s => p in HP_TAUT
proof
let s, q, p be Element of HP-WFF ; ::_thesis: ( s => (q => p) in HP_TAUT & q in HP_TAUT implies s => p in HP_TAUT )
assume that
A1: s => (q => p) in HP_TAUT and
A2: q in HP_TAUT ; ::_thesis: s => p in HP_TAUT
 (s => (q => p)) => (q => (s => p)) in HP_TAUT by Th26;
then  q => (s => p) in HP_TAUT by A1, Def10;
hence  s => p in HP_TAUT by A2, Def10; ::_thesis: verum
end;

begin

theorem Th30: :: HILBERT1:30
for p being Element of HP-WFF holds p => (p '&' p) in HP_TAUT
proof
let p be Element of HP-WFF ; ::_thesis: p => (p '&' p) in HP_TAUT
A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in HP_TAUT by Th27;
 p => (p => (p '&' p)) in HP_TAUT by Def10;
hence  p => (p '&' p) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th31: :: HILBERT1:31
for p, q being Element of HP-WFF holds
( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )
hereby  ::_thesis: ( p in HP_TAUT & q in HP_TAUT implies p '&' q in HP_TAUT )
A1: (p '&' q) => q in HP_TAUT by Def10;
assume A2: p '&' q in HP_TAUT ; ::_thesis: ( p in HP_TAUT & q in HP_TAUT )
 (p '&' q) => p in HP_TAUT by Def10;
hence  ( p in HP_TAUT & q in HP_TAUT ) by A2, A1, Def10; ::_thesis: verum
end;
assume that
A3: p in HP_TAUT and
A4: q in HP_TAUT ; ::_thesis: p '&' q in HP_TAUT
 p => (q => (p '&' q)) in HP_TAUT by Def10;
then  q => (p '&' q) in HP_TAUT by A3, Def10;
hence  p '&' q in HP_TAUT by A4, Def10; ::_thesis: verum
end;

theorem :: HILBERT1:32
for p, q being Element of HP-WFF st p '&' q in HP_TAUT holds
q '&' p in HP_TAUT
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in HP_TAUT implies q '&' p in HP_TAUT )
assume A1: p '&' q in HP_TAUT ; ::_thesis: q '&' p in HP_TAUT
then A2: q in HP_TAUT by Th31;
 p in HP_TAUT by A1, Th31;
hence  q '&' p in HP_TAUT by A2, Th31; ::_thesis: verum
end;

theorem Th33: :: HILBERT1:33
for p, q, r being Element of HP-WFF holds ((p '&' q) => r) => (p => (q => r)) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ((p '&' q) => r) => (p => (q => r)) in HP_TAUT
set qp = q => (p '&' q);
set pr = ((p '&' q) => r) => (q => r);
A1: (p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r)))) => ((p => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r)))) in HP_TAUT by Def10;
A2: p => (q => (p '&' q)) in HP_TAUT by Def10;
 p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r))) in HP_TAUT by Th15, Th21;
then  (p => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r))) in HP_TAUT by A1, Def10;
then A3: p => (((p '&' q) => r) => (q => r)) in HP_TAUT by A2, Def10;
 (p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r))) in HP_TAUT by Th26;
hence  ((p '&' q) => r) => (p => (q => r)) in HP_TAUT by A3, Def10; ::_thesis: verum
end;

theorem Th34: :: HILBERT1:34
for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p '&' q) => r) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((p '&' q) => r) in HP_TAUT
A1: ((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) in HP_TAUT by Th21;
 (p '&' q) => q in HP_TAUT by Def10;
then  (q => r) => ((p '&' q) => r) in HP_TAUT by A1, Def10;
then A2: p => ((q => r) => ((p '&' q) => r)) in HP_TAUT by Th15;
A3: (p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) in HP_TAUT by Th26;
 (p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) in HP_TAUT by Def10;
then  (p => (q => r)) => (p => ((p '&' q) => r)) in HP_TAUT by A2, Def10;
then A4: (p => (q => r)) => ((p '&' q) => (p => r)) in HP_TAUT by A3, Th23;
A5: (p '&' q) => p in HP_TAUT by Def10;
 ((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) in HP_TAUT by Def10;
then  ((p '&' q) => (p => r)) => ((p '&' q) => r) in HP_TAUT by A5, Th29;
hence  (p => (q => r)) => ((p '&' q) => r) in HP_TAUT by A4, Th23; ::_thesis: verum
end;

theorem Th35: :: HILBERT1:35
for r, p, q being Element of HP-WFF holds (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT
proof
let r, p, q be Element of HP-WFF ; ::_thesis: (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT
A1: (r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q))) in HP_TAUT by Def10;
 p => (q => (p '&' q)) in HP_TAUT by Def10;
then A2: r => (p => (q => (p '&' q))) in HP_TAUT by Th15;
 (r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q)))) in HP_TAUT by Def10;
then  (r => p) => (r => (q => (p '&' q))) in HP_TAUT by A2, Def10;
hence  (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

theorem Th36: :: HILBERT1:36
for p, q being Element of HP-WFF holds ((p => q) '&' p) => q in HP_TAUT
proof
let p, q be Element of HP-WFF ; ::_thesis: ((p => q) '&' p) => q in HP_TAUT
set P = p => q;
A1: (p => q) => (p => q) in HP_TAUT by Th14;
 ((p => q) => (p => q)) => (((p => q) '&' p) => q) in HP_TAUT by Th34;
hence  ((p => q) '&' p) => q in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem :: HILBERT1:37
for p, q, s being Element of HP-WFF holds (((p => q) '&' p) '&' s) => q in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (((p => q) '&' p) '&' s) => q in HP_TAUT
set P = (p => q) '&' p;
A1: ((p => q) '&' p) => q in HP_TAUT by Th36;
 (((p => q) '&' p) '&' s) => ((p => q) '&' p) in HP_TAUT by Def10;
hence  (((p => q) '&' p) '&' s) => q in HP_TAUT by A1, Th23; ::_thesis: verum
end;

theorem :: HILBERT1:38
for q, s, p being Element of HP-WFF holds (q => s) => ((p '&' q) => s) in HP_TAUT
proof
let q, s, p be Element of HP-WFF ; ::_thesis: (q => s) => ((p '&' q) => s) in HP_TAUT
set P = p '&' q;
A1: (p '&' q) => q in HP_TAUT by Def10;
 ((p '&' q) => q) => ((q => s) => ((p '&' q) => s)) in HP_TAUT by Th21;
hence  (q => s) => ((p '&' q) => s) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th39: :: HILBERT1:39
for q, s, p being Element of HP-WFF holds (q => s) => ((q '&' p) => s) in HP_TAUT
proof
let q, s, p be Element of HP-WFF ; ::_thesis: (q => s) => ((q '&' p) => s) in HP_TAUT
set P = q '&' p;
A1: (q '&' p) => q in HP_TAUT by Def10;
 ((q '&' p) => q) => ((q => s) => ((q '&' p) => s)) in HP_TAUT by Th21;
hence  (q => s) => ((q '&' p) => s) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th40: :: HILBERT1:40
for p, s, q being Element of HP-WFF holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof
let p, s, q be Element of HP-WFF ; ::_thesis: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
set P = p '&' s;
A1: ((p '&' s) => q) => (((p '&' s) => s) => ((p '&' s) => (q '&' s))) in HP_TAUT by Th35;
 (p '&' s) => s in HP_TAUT by Def10;
hence  ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by A1, Th29; ::_thesis: verum
end;

theorem Th41: :: HILBERT1:41
for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
A1: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th40;
 (p => q) => ((p '&' s) => q) in HP_TAUT by Th39;
hence  (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

theorem Th42: :: HILBERT1:42
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT
set P = p => q;
set Q = p '&' s;
set S = q '&' s;
A1: (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th41;
 ((p => q) => ((p '&' s) => (q '&' s))) => (((p => q) '&' (p '&' s)) => (q '&' s)) in HP_TAUT by Th34;
hence  ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th43: :: HILBERT1:43
for p, q being Element of HP-WFF holds (p '&' q) => (q '&' p) in HP_TAUT
proof
let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => (q '&' p) in HP_TAUT
set P = p '&' q;
A1: (p '&' q) => q in HP_TAUT by Def10;
A2: (p '&' q) => p in HP_TAUT by Def10;
 ((p '&' q) => q) => (((p '&' q) => p) => ((p '&' q) => (q '&' p))) in HP_TAUT by Th35;
then  ((p '&' q) => p) => ((p '&' q) => (q '&' p)) in HP_TAUT by A1, Def10;
hence  (p '&' q) => (q '&' p) in HP_TAUT by A2, Def10; ::_thesis: verum
end;

theorem Th44: :: HILBERT1:44
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT
A1: (q '&' s) => (s '&' q) in HP_TAUT by Th43;
 ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT by Th42;
hence  ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

theorem Th45: :: HILBERT1:45
for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
A1: ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT by Th44;
 (((p => q) '&' (p '&' s)) => (s '&' q)) => ((p => q) => ((p '&' s) => (s '&' q))) in HP_TAUT by Th33;
hence  (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem Th46: :: HILBERT1:46
for p, q, s being Element of HP-WFF holds (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
set T = s '&' p;
A1: (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT by Th45;
A2: (s '&' p) => (p '&' s) in HP_TAUT by Th43;
 ((p => q) => ((p '&' s) => (s '&' q))) => (((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q)))) in HP_TAUT by Th24;
then  ((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q))) in HP_TAUT by A1, Def10;
hence  (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT by A2, Def10; ::_thesis: verum
end;

theorem :: HILBERT1:47
for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
proof
let p, s, q be Element of HP-WFF ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43;
 ((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT by Th46;
hence  (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem :: HILBERT1:48
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT
set P = p => q;
set Q = p => s;
set S = p => (q '&' s);
A1: (p => q) => ((p => s) => (p => (q '&' s))) in HP_TAUT by Th35;
 ((p => q) => ((p => s) => (p => (q '&' s)))) => (((p => q) '&' (p => s)) => (p => (q '&' s))) in HP_TAUT by Th34;
hence  ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

Lm5:  for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => q in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => q in HP_TAUT
A1: (p '&' q) => q in HP_TAUT by Def10;
 ((p '&' q) '&' s) => (p '&' q) in HP_TAUT by Def10;
hence  ((p '&' q) '&' s) => q in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm6:  for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT
set P = (p '&' q) '&' s;
A1: ((p '&' q) '&' s) => q in HP_TAUT by Lm5;
 (((p '&' q) '&' s) => q) => ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in HP_TAUT by Th46;
hence  (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

Lm7:  for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT
A1: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT by Lm6;
 ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) in HP_TAUT by Th30;
hence  ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm8:  for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' s) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' s) in HP_TAUT
set P = p '&' q;
A1: (p '&' q) => p in HP_TAUT by Def10;
 ((p '&' q) => p) => (((p '&' q) '&' s) => (p '&' s)) in HP_TAUT by Th41;
hence  ((p '&' q) '&' s) => (p '&' s) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

Lm9:  for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT
set P = (p '&' q) '&' s;
set Q = p '&' s;
A1: ((p '&' q) '&' s) => (p '&' s) in HP_TAUT by Lm8;
 (((p '&' q) '&' s) => (p '&' s)) => ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in HP_TAUT by Th41;
hence  (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

Lm10:  for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT
A1: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT by Lm9;
 ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT by Lm7;
hence  ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm11:  for p, s, q being Element of HP-WFF holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT
proof
let p, s, q be Element of HP-WFF ; ::_thesis: ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT
set P = p '&' s;
set Q = s '&' p;
A1: (p '&' s) => (s '&' p) in HP_TAUT by Th43;
 ((p '&' s) => (s '&' p)) => (((p '&' s) '&' q) => ((s '&' p) '&' q)) in HP_TAUT by Th41;
hence  ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

Lm12:  for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT
A1: ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT by Lm11;
 ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT by Lm10;
hence  ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm13:  for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT
A1: ((s '&' p) '&' q) => ((s '&' q) '&' p) in HP_TAUT by Lm10;
 ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT by Lm12;
hence  ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm14:  for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT
A1: ((s '&' q) '&' p) => (p '&' (s '&' q)) in HP_TAUT by Th43;
 ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT by Lm13;
hence  ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm15:  for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
proof
let p, s, q be Element of HP-WFF ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43;
 ((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT by Th46;
hence  (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem :: HILBERT1:49
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT
A1: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by Lm15;
 ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT by Lm14;
hence  ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm16:  for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT
A1: (p '&' (s '&' q)) => ((s '&' q) '&' p) in HP_TAUT by Th43;
 (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by Lm15;
hence  (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm17:  for s, q, p being Element of HP-WFF holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT
proof
let s, q, p be Element of HP-WFF ; ::_thesis: ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43;
 ((s '&' q) => (q '&' s)) => (((s '&' q) '&' p) => ((q '&' s) '&' p)) in HP_TAUT by Th41;
hence  ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

Lm18:  for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT
A1: ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT by Lm17;
 (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT by Lm16;
hence  (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm19:  for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT
A1: ((q '&' s) '&' p) => ((p '&' s) '&' q) in HP_TAUT by Lm13;
 (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT by Lm18;
hence  (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;

Lm20:  for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT
set P = q '&' s;
set Q = s '&' q;
A1: (q '&' s) => (s '&' q) in HP_TAUT by Th43;
 ((q '&' s) => (s '&' q)) => ((p '&' (q '&' s)) => (p '&' (s '&' q))) in HP_TAUT by Th46;
hence  (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;

theorem :: HILBERT1:50
for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT
A1: (p '&' (s '&' q)) => ((p '&' q) '&' s) in HP_TAUT by Lm19;
 (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by Lm20;
hence  (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT by A1, Th23; ::_thesis: verum
end;