:: CQC_THE3 semantic presentation

begin


theorem Th1: :: CQC_THE3:1
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p in X holds
X |- p
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p in X holds
X |- p
let p be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p in X holds
X |- p
let X be Subset of (CQC-WFF A); ::_thesis: ( p in X implies X |- p )
 X c= Cn X by CQC_THE1:17;
hence  ( p in X implies X |- p ) by CQC_THE1:def_8; ::_thesis: verum
end;

theorem Th2: :: CQC_THE3:2
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) st X c= Cn Y holds
Cn X c= Cn Y by CQC_THE1:15, CQC_THE1:16;

theorem Th3: :: CQC_THE3:3
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p & {p} |- q holds
X |- q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p & {p} |- q holds
X |- q
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p & {p} |- q holds
X |- q
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p & {p} |- q implies X |- q )
assume that
A1: X |- p and
A2: {p} |- q ; ::_thesis: X |- q
 p in Cn X by A1, CQC_THE1:def_8;
then  {p} c= Cn X by ZFMISC_1:31;
then A3: Cn {p} c= Cn X by CQC_THE1:15, CQC_THE1:16;
 q in Cn {p} by A2, CQC_THE1:def_8;
hence  X |- q by A3, CQC_THE1:def_8; ::_thesis: verum
end;

theorem Th4: :: CQC_THE3:4
for A being QC-alphabet
for p being Element of CQC-WFF A
for X, Y being Subset of (CQC-WFF A) st X |- p & X c= Y holds
Y |- p
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for X, Y being Subset of (CQC-WFF A) st X |- p & X c= Y holds
Y |- p
let p be Element of CQC-WFF A; ::_thesis: for X, Y being Subset of (CQC-WFF A) st X |- p & X c= Y holds
Y |- p
let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X |- p & X c= Y implies Y |- p )
assume that
A1: X |- p and
A2: X c= Y ; ::_thesis: Y |- p
A3: p in Cn X by A1, CQC_THE1:def_8;
 Cn X c= Cn Y by A2, CQC_THE1:18;
hence  Y |- p by A3, CQC_THE1:def_8; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
predp |- q means :Def1: :: CQC_THE3:def 1
{p} |- q;
end;

:: deftheorem Def1 defines |- CQC_THE3:def_1_:_
 for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p |- q iff {p} |- q );

theorem Th5: :: CQC_THE3:5
for A being QC-alphabet
for p being Element of CQC-WFF A holds p |- p
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p |- p
let p be Element of CQC-WFF A; ::_thesis: p |- p
 {p} |- p by CQC_THE2:87;
hence  p |- p by Def1; ::_thesis: verum
end;

theorem Th6: :: CQC_THE3:6
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p |- q & q |- r holds
p |- r
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p |- q & q |- r holds
p |- r
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p |- q & q |- r implies p |- r )
assume that
A1: p |- q and
A2: q |- r ; ::_thesis: p |- r
A3: {q} |- r by A2, Def1;
 {p} |- q by A1, Def1;
then  {p} |- r by A3, Th3;
hence  p |- r by Def1; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let X, Y be Subset of (CQC-WFF A);
predX |- Y means :Def2: :: CQC_THE3:def 2
 for p being Element of CQC-WFF A st p in Y holds
X |- p;
end;

:: deftheorem Def2 defines |- CQC_THE3:def_2_:_
 for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |- Y iff for p being Element of CQC-WFF A st p in Y holds
X |- p );

theorem Th7: :: CQC_THE3:7
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |- Y iff Y c= Cn X )
proof
let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds
( X |- Y iff Y c= Cn X )
let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X |- Y iff Y c= Cn X )
A1: now__::_thesis:_(_X_|-_Y_implies_Y_c=_Cn_X_)
assume A2: X |- Y ; ::_thesis: Y c= Cn X
now__::_thesis:_for_p_being_set_st_p_in_Y_holds_
p_in_Cn_X
let p be set ; ::_thesis: ( p in Y implies p in Cn X )
assume A3: p in Y ; ::_thesis: p in Cn X
then reconsider p9 = p as Element of CQC-WFF A ;
 X |- p9 by A2, A3, Def2;
hence  p in Cn X by CQC_THE1:def_8; ::_thesis: verum
end;
hence  Y c= Cn X by TARSKI:def_3; ::_thesis: verum
end;
now__::_thesis:_(_Y_c=_Cn_X_implies_X_|-_Y_)
assume  Y c= Cn X ; ::_thesis: X |- Y
then  for p being Element of CQC-WFF A st p in Y holds
X |- p by CQC_THE1:def_8;
hence  X |- Y by Def2; ::_thesis: verum
end;
hence  ( X |- Y iff Y c= Cn X ) by A1; ::_thesis: verum
end;

theorem :: CQC_THE3:8
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds X |- X
proof
let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds X |- X
let X be Subset of (CQC-WFF A); ::_thesis: X |- X
 for p being Element of CQC-WFF A st p in X holds
X |- p by Th1;
hence  X |- X by Def2; ::_thesis: verum
end;

theorem Th9: :: CQC_THE3:9
for A being QC-alphabet
for X, Y, Z being Subset of (CQC-WFF A) st X |- Y & Y |- Z holds
X |- Z
proof
let A be QC-alphabet ; ::_thesis: for X, Y, Z being Subset of (CQC-WFF A) st X |- Y & Y |- Z holds
X |- Z
let X, Y, Z be Subset of (CQC-WFF A); ::_thesis: ( X |- Y & Y |- Z implies X |- Z )
assume that
A1: X |- Y and
A2: Y |- Z ; ::_thesis: X |- Z
 for p being Element of CQC-WFF A st p in Z holds
X |- p
proof
let p be Element of CQC-WFF A; ::_thesis: ( p in Z implies X |- p )
assume  p in Z ; ::_thesis: X |- p
then  Y |- p by A2, Def2;
then A3: p in Cn Y by CQC_THE1:def_8;
 Y c= Cn X by A1, Th7;
then  Cn Y c= Cn X by CQC_THE1:15, CQC_THE1:16;
hence  X |- p by A3, CQC_THE1:def_8; ::_thesis: verum
end;
hence  X |- Z by Def2; ::_thesis: verum
end;

theorem Th10: :: CQC_THE3:10
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- {p} iff X |- p )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- {p} iff X |- p )
let p be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) holds
( X |- {p} iff X |- p )
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- {p} iff X |- p )
A1: now__::_thesis:_(_X_|-_p_implies_X_|-_{p}_)
assume  X |- p ; ::_thesis: X |- {p}
then  for q being Element of CQC-WFF A st q in {p} holds
X |- q by TARSKI:def_1;
hence  X |- {p} by Def2; ::_thesis: verum
end;
now__::_thesis:_(_X_|-_{p}_implies_X_|-_p_)
A2: p in {p} by TARSKI:def_1;
assume  X |- {p} ; ::_thesis: X |- p
hence  X |- p by A2, Def2; ::_thesis: verum
end;
hence  ( X |- {p} iff X |- p ) by A1; ::_thesis: verum
end;

theorem Th11: :: CQC_THE3:11
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( {p} |- {q} iff p |- q )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( {p} |- {q} iff p |- q )
let p, q be Element of CQC-WFF A; ::_thesis: ( {p} |- {q} iff p |- q )
A1: now__::_thesis:_(_p_|-_q_implies_{p}_|-_{q}_)
assume  p |- q ; ::_thesis: {p} |- {q}
then  {p} |- q by Def1;
hence  {p} |- {q} by Th10; ::_thesis: verum
end;
now__::_thesis:_(_{p}_|-_{q}_implies_p_|-_q_)
assume  {p} |- {q} ; ::_thesis: p |- q
then  {p} |- q by Th10;
hence  p |- q by Def1; ::_thesis: verum
end;
hence  ( {p} |- {q} iff p |- q ) by A1; ::_thesis: verum
end;

theorem :: CQC_THE3:12
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) st X c= Y holds
Y |- X
proof
let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) st X c= Y holds
Y |- X
let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X c= Y implies Y |- X )
assume  X c= Y ; ::_thesis: Y |- X
then  for p being Element of CQC-WFF A st p in X holds
Y |- p by Th1;
hence  Y |- X by Def2; ::_thesis: verum
end;

theorem Th13: :: CQC_THE3:13
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds X |- TAUT A
proof
let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds X |- TAUT A
let X be Subset of (CQC-WFF A); ::_thesis: X |- TAUT A
 TAUT A c= Cn X by CQC_THE1:39;
hence  X |- TAUT A by Th7; ::_thesis: verum
end;

theorem :: CQC_THE3:14
for A being QC-alphabet holds {} (CQC-WFF A) |- TAUT A by Th13;

definition
let A be QC-alphabet ;
let X be Subset of (CQC-WFF A);
pred |- X means :Def3: :: CQC_THE3:def 3
 for p being Element of CQC-WFF A st p in X holds
p is valid ;
end;

:: deftheorem Def3 defines |- CQC_THE3:def_3_:_
 for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds
( |- X iff for p being Element of CQC-WFF A st p in X holds
p is valid );

theorem Th15: :: CQC_THE3:15
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds
( |- X iff {} (CQC-WFF A) |- X )
proof
let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds
( |- X iff {} (CQC-WFF A) |- X )
let X be Subset of (CQC-WFF A); ::_thesis: ( |- X iff {} (CQC-WFF A) |- X )
A1: now__::_thesis:_(_{}_(CQC-WFF_A)_|-_X_implies_|-_X_)
assume A2: {} (CQC-WFF A) |- X ; ::_thesis: |- X
now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_X_holds_
p_is_valid
let p be Element of CQC-WFF A; ::_thesis: ( p in X implies p is valid )
assume  p in X ; ::_thesis: p is valid
then  {} (CQC-WFF A) |- p by A2, Def2;
hence  p is valid by CQC_THE1:def_9; ::_thesis: verum
end;
hence  |- X by Def3; ::_thesis: verum
end;
now__::_thesis:_(_|-_X_implies_{}_(CQC-WFF_A)_|-_X_)
assume A3: |- X ; ::_thesis: {} (CQC-WFF A) |- X
now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_X_holds_
{}_(CQC-WFF_A)_|-_p
let p be Element of CQC-WFF A; ::_thesis: ( p in X implies {} (CQC-WFF A) |- p )
assume  p in X ; ::_thesis: {} (CQC-WFF A) |- p
then  p is valid by A3, Def3;
hence  {} (CQC-WFF A) |- p by CQC_THE1:def_9; ::_thesis: verum
end;
hence  {} (CQC-WFF A) |- X by Def2; ::_thesis: verum
end;
hence  ( |- X iff {} (CQC-WFF A) |- X ) by A1; ::_thesis: verum
end;

theorem :: CQC_THE3:16
for A being QC-alphabet holds |- TAUT A
proof
let A be QC-alphabet ; ::_thesis: |- TAUT A
A1: ( |- TAUT A iff {} (CQC-WFF A) |- TAUT A ) by Th15;
 {} (CQC-WFF A) |- TAUT A by Th13;
hence  |- TAUT A by A1; ::_thesis: verum
end;

theorem :: CQC_THE3:17
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds
( |- X iff X c= TAUT A )
proof
let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds
( |- X iff X c= TAUT A )
let X be Subset of (CQC-WFF A); ::_thesis: ( |- X iff X c= TAUT A )
A1: now__::_thesis:_(_|-_X_implies_X_c=_TAUT_A_)
assume A2: |- X ; ::_thesis: X c= TAUT A
now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_X_holds_
p_in_TAUT_A
let p be Element of CQC-WFF A; ::_thesis: ( p in X implies p in TAUT A )
assume  p in X ; ::_thesis: p in TAUT A
then  p is valid by A2, Def3;
hence  p in TAUT A by CQC_THE1:def_10; ::_thesis: verum
end;
hence  X c= TAUT A by SUBSET_1:2; ::_thesis: verum
end;
now__::_thesis:_(_X_c=_TAUT_A_implies_|-_X_)
assume  X c= TAUT A ; ::_thesis: |- X
then  for p being Element of CQC-WFF A st p in X holds
p is valid by CQC_THE1:def_10;
hence  |- X by Def3; ::_thesis: verum
end;
hence  ( |- X iff X c= TAUT A ) by A1; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let X, Y be Subset of (CQC-WFF A);
predX |-| Y means :Def4: :: CQC_THE3:def 4
 for p being Element of CQC-WFF A holds
( X |- p iff Y |- p );
reflexivity
 for X being Subset of (CQC-WFF A)
for p being Element of CQC-WFF A holds
( X |- p iff X |- p ) ;
symmetry
 for X, Y being Subset of (CQC-WFF A) st ( for p being Element of CQC-WFF A holds
( X |- p iff Y |- p ) ) holds
for p being Element of CQC-WFF A holds
( Y |- p iff X |- p ) ;
end;

:: deftheorem Def4 defines |-| CQC_THE3:def_4_:_
 for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff for p being Element of CQC-WFF A holds
( X |- p iff Y |- p ) );

theorem Th18: :: CQC_THE3:18
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff ( X |- Y & Y |- X ) )
proof
let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff ( X |- Y & Y |- X ) )
let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X |-| Y iff ( X |- Y & Y |- X ) )
A1: now__::_thesis:_(_X_|-_Y_&_Y_|-_X_implies_X_|-|_Y_)
assume that
A2: X |- Y and
A3: Y |- X ; ::_thesis: X |-| Y
now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_holds_
(_X_|-_p_iff_Y_|-_p_)
let p be Element of CQC-WFF A; ::_thesis: ( X |- p iff Y |- p )
A4: now__::_thesis:_(_Y_|-_p_implies_X_|-_p_)
assume  Y |- p ; ::_thesis: X |- p
then  Y |- {p} by Th10;
then  X |- {p} by A2, Th9;
hence  X |- p by Th10; ::_thesis: verum
end;
now__::_thesis:_(_X_|-_p_implies_Y_|-_p_)
assume  X |- p ; ::_thesis: Y |- p
then  X |- {p} by Th10;
then  Y |- {p} by A3, Th9;
hence  Y |- p by Th10; ::_thesis: verum
end;
hence  ( X |- p iff Y |- p ) by A4; ::_thesis: verum
end;
hence  X |-| Y by Def4; ::_thesis: verum
end;
now__::_thesis:_(_X_|-|_Y_implies_(_X_|-_Y_&_Y_|-_X_)_)
assume A5: X |-| Y ; ::_thesis: ( X |- Y & Y |- X )
now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_Y_holds_
X_|-_p
let p be Element of CQC-WFF A; ::_thesis: ( p in Y implies X |- p )
assume  p in Y ; ::_thesis: X |- p
then  Y |- p by Th1;
hence  X |- p by A5, Def4; ::_thesis: verum
end;
hence  X |- Y by Def2; ::_thesis: Y |- X
now__::_thesis:_for_p_being_Element_of_CQC-WFF_A_st_p_in_X_holds_
Y_|-_p
let p be Element of CQC-WFF A; ::_thesis: ( p in X implies Y |- p )
assume  p in X ; ::_thesis: Y |- p
then  X |- p by Th1;
hence  Y |- p by A5, Def4; ::_thesis: verum
end;
hence  Y |- X by Def2; ::_thesis: verum
end;
hence  ( X |-| Y iff ( X |- Y & Y |- X ) ) by A1; ::_thesis: verum
end;

theorem Th19: :: CQC_THE3:19
for A being QC-alphabet
for X, Y, Z being Subset of (CQC-WFF A) st X |-| Y & Y |-| Z holds
X |-| Z
proof
let A be QC-alphabet ; ::_thesis: for X, Y, Z being Subset of (CQC-WFF A) st X |-| Y & Y |-| Z holds
X |-| Z
let X, Y, Z be Subset of (CQC-WFF A); ::_thesis: ( X |-| Y & Y |-| Z implies X |-| Z )
assume that
A1: X |-| Y and
A2: Y |-| Z ; ::_thesis: X |-| Z
A3: Z |- Y by A2, Th18;
 Y |- X by A1, Th18;
then A4: Z |- X by A3, Th9;
A5: Y |- Z by A2, Th18;
 X |- Y by A1, Th18;
then  X |- Z by A5, Th9;
hence  X |-| Z by A4, Th18; ::_thesis: verum
end;

theorem Th20: :: CQC_THE3:20
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff Cn X = Cn Y )
proof
let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff Cn X = Cn Y )
let X, Y be Subset of (CQC-WFF A); ::_thesis: ( X |-| Y iff Cn X = Cn Y )
A1: now__::_thesis:_(_X_|-|_Y_implies_Cn_X_=_Cn_Y_)
assume A2: X |-| Y ; ::_thesis: Cn X = Cn Y
then  Y |- X by Th18;
then  X c= Cn Y by Th7;
then A3: Cn X c= Cn Y by CQC_THE1:15, CQC_THE1:16;
 X |- Y by A2, Th18;
then  Y c= Cn X by Th7;
then  Cn Y c= Cn X by CQC_THE1:15, CQC_THE1:16;
hence  Cn X = Cn Y by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_(_Cn_X_=_Cn_Y_implies_X_|-|_Y_)
assume A4: Cn X = Cn Y ; ::_thesis: X |-| Y
 X c= Cn X by CQC_THE1:17;
then A5: Y |- X by A4, Th7;
 Y c= Cn Y by CQC_THE1:17;
then  X |- Y by A4, Th7;
hence  X |-| Y by A5, Th18; ::_thesis: verum
end;
hence  ( X |-| Y iff Cn X = Cn Y ) by A1; ::_thesis: verum
end;

Lm1:  for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds X \/ Y c= (Cn X) \/ (Cn Y)
proof
let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds X \/ Y c= (Cn X) \/ (Cn Y)
let X, Y be Subset of (CQC-WFF A); ::_thesis: X \/ Y c= (Cn X) \/ (Cn Y)
A1: Y c= Cn Y by CQC_THE1:17;
 X c= Cn X by CQC_THE1:17;
hence  X \/ Y c= (Cn X) \/ (Cn Y) by A1, XBOOLE_1:13; ::_thesis: verum
end;

theorem Th21: :: CQC_THE3:21
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds (Cn X) \/ (Cn Y) c= Cn (X \/ Y)
proof
let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds (Cn X) \/ (Cn Y) c= Cn (X \/ Y)
let X, Y be Subset of (CQC-WFF A); ::_thesis: (Cn X) \/ (Cn Y) c= Cn (X \/ Y)
A1: Cn Y c= Cn (X \/ Y) by CQC_THE1:18, XBOOLE_1:7;
 Cn X c= Cn (X \/ Y) by CQC_THE1:18, XBOOLE_1:7;
hence  (Cn X) \/ (Cn Y) c= Cn (X \/ Y) by A1, XBOOLE_1:8; ::_thesis: verum
end;

theorem Th22: :: CQC_THE3:22
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y))
proof
let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y))
let X, Y be Subset of (CQC-WFF A); ::_thesis: Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y))
A1: Cn (X \/ Y) c= Cn ((Cn X) \/ (Cn Y)) by Lm1, CQC_THE1:18;
 Cn ((Cn X) \/ (Cn Y)) c= Cn (X \/ Y) by Th2, Th21;
hence  Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: CQC_THE3:23
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds X |-| Cn X
proof
let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) holds X |-| Cn X
let X be Subset of (CQC-WFF A); ::_thesis: X |-| Cn X
 Cn X = Cn (Cn X) by CQC_THE1:19;
hence  X |-| Cn X by Th20; ::_thesis: verum
end;

theorem :: CQC_THE3:24
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds X \/ Y |-| (Cn X) \/ (Cn Y)
proof
let A be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF A) holds X \/ Y |-| (Cn X) \/ (Cn Y)
let X, Y be Subset of (CQC-WFF A); ::_thesis: X \/ Y |-| (Cn X) \/ (Cn Y)
 Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y)) by Th22;
hence  X \/ Y |-| (Cn X) \/ (Cn Y) by Th20; ::_thesis: verum
end;

theorem Th25: :: CQC_THE3:25
for A being QC-alphabet
for X1, X2, Y being Subset of (CQC-WFF A) st X1 |-| X2 holds
X1 \/ Y |-| X2 \/ Y
proof
let A be QC-alphabet ; ::_thesis: for X1, X2, Y being Subset of (CQC-WFF A) st X1 |-| X2 holds
X1 \/ Y |-| X2 \/ Y
let X1, X2, Y be Subset of (CQC-WFF A); ::_thesis: ( X1 |-| X2 implies X1 \/ Y |-| X2 \/ Y )
assume  X1 |-| X2 ; ::_thesis: X1 \/ Y |-| X2 \/ Y
then  Cn X1 = Cn X2 by Th20;
then  Cn (X1 \/ Y) = Cn ((Cn X2) \/ (Cn Y)) by Th22
.= Cn (X2 \/ Y) by Th22 ;
hence  X1 \/ Y |-| X2 \/ Y by Th20; ::_thesis: verum
end;

theorem Th26: :: CQC_THE3:26
for A being QC-alphabet
for X1, X2, Y, Z being Subset of (CQC-WFF A) st X1 |-| X2 & X1 \/ Y |- Z holds
X2 \/ Y |- Z
proof
let A be QC-alphabet ; ::_thesis: for X1, X2, Y, Z being Subset of (CQC-WFF A) st X1 |-| X2 & X1 \/ Y |- Z holds
X2 \/ Y |- Z
let X1, X2, Y, Z be Subset of (CQC-WFF A); ::_thesis: ( X1 |-| X2 & X1 \/ Y |- Z implies X2 \/ Y |- Z )
assume that
A1: X1 |-| X2 and
A2: X1 \/ Y |- Z ; ::_thesis: X2 \/ Y |- Z
 X1 \/ Y |-| X2 \/ Y by A1, Th25;
then  Cn (X1 \/ Y) = Cn (X2 \/ Y) by Th20;
then  Z c= Cn (X2 \/ Y) by A2, Th7;
hence  X2 \/ Y |- Z by Th7; ::_thesis: verum
end;

theorem Th27: :: CQC_THE3:27
for A being QC-alphabet
for X1, X2, Y being Subset of (CQC-WFF A) st X1 |-| X2 & Y |- X1 holds
Y |- X2
proof
let A be QC-alphabet ; ::_thesis: for X1, X2, Y being Subset of (CQC-WFF A) st X1 |-| X2 & Y |- X1 holds
Y |- X2
let X1, X2, Y be Subset of (CQC-WFF A); ::_thesis: ( X1 |-| X2 & Y |- X1 implies Y |- X2 )
assume that
A1: X1 |-| X2 and
A2: Y |- X1 ; ::_thesis: Y |- X2
 X1 |- X2 by A1, Th18;
hence  Y |- X2 by A2, Th9; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
predp |-| q means :Def5: :: CQC_THE3:def 5
( p |- q & q |- p );
reflexivity
 for p being Element of CQC-WFF A holds
( p |- p & p |- p ) by Th5;
symmetry
 for p, q being Element of CQC-WFF A st p |- q & q |- p holds
( q |- p & p |- q ) ;
end;

:: deftheorem Def5 defines |-| CQC_THE3:def_5_:_
 for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p |-| q iff ( p |- q & q |- p ) );

theorem Th28: :: CQC_THE3:28
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p |-| q & q |-| r holds
p |-| r
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p |-| q & q |-| r holds
p |-| r
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p |-| q & q |-| r implies p |-| r )
assume that
A1: p |-| q and
A2: q |-| r ; ::_thesis: p |-| r
A3: r |- q by A2, Def5;
 q |- p by A1, Def5;
then A4: r |- p by A3, Th6;
A5: q |- r by A2, Def5;
 p |- q by A1, Def5;
then  p |- r by A5, Th6;
hence  p |-| r by A4, Def5; ::_thesis: verum
end;

theorem Th29: :: CQC_THE3:29
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p |-| q iff {p} |-| {q} )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( p |-| q iff {p} |-| {q} )
let p, q be Element of CQC-WFF A; ::_thesis: ( p |-| q iff {p} |-| {q} )
A1: now__::_thesis:_(_{p}_|-|_{q}_implies_p_|-|_q_)
assume A2: {p} |-| {q} ; ::_thesis: p |-| q
then  {q} |- {p} by Th18;
then A3: q |- p by Th11;
 {p} |- {q} by A2, Th18;
then  p |- q by Th11;
hence  p |-| q by A3, Def5; ::_thesis: verum
end;
now__::_thesis:_(_p_|-|_q_implies_{p}_|-|_{q}_)
assume A4: p |-| q ; ::_thesis: {p} |-| {q}
then  q |- p by Def5;
then A5: {q} |- {p} by Th11;
 p |- q by A4, Def5;
then  {p} |- {q} by Th11;
hence  {p} |-| {q} by A5, Th18; ::_thesis: verum
end;
hence  ( p |-| q iff {p} |-| {q} ) by A1; ::_thesis: verum
end;

theorem :: CQC_THE3:30
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p |-| q & X |- p holds
X |- q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p |-| q & X |- p holds
X |- q
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p |-| q & X |- p holds
X |- q
let X be Subset of (CQC-WFF A); ::_thesis: ( p |-| q & X |- p implies X |- q )
assume that
A1: p |-| q and
A2: X |- p ; ::_thesis: X |- q
A3: X |- {p} by A2, Th10;
 {p} |-| {q} by A1, Th29;
then  X |- {q} by A3, Th27;
hence  X |- q by Th10; ::_thesis: verum
end;

theorem Th31: :: CQC_THE3:31
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds {p,q} |-| {(p '&' q)}
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds {p,q} |-| {(p '&' q)}
let p, q be Element of CQC-WFF A; ::_thesis: {p,q} |-| {(p '&' q)}
 for r being Element of CQC-WFF A holds
( {p,q} |- r iff {(p '&' q)} |- r ) by CQC_THE2:89;
hence  {p,q} |-| {(p '&' q)} by Def4; ::_thesis: verum
end;

theorem :: CQC_THE3:32
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p '&' q |-| q '&' p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p '&' q |-| q '&' p
let p, q be Element of CQC-WFF A; ::_thesis: p '&' q |-| q '&' p
A1: {q,p} |-| {(q '&' p)} by Th31;
 {(p '&' q)} |-| {q,p} by Th31;
then  {(p '&' q)} |-| {(q '&' p)} by A1, Th19;
hence  p '&' q |-| q '&' p by Th29; ::_thesis: verum
end;

Lm2:  for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p & X |- q holds
X |- p '&' q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p & X |- q holds
X |- p '&' q
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p & X |- q holds
X |- p '&' q
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p & X |- q implies X |- p '&' q )
assume that
A1: X |- p and
A2: X |- q ; ::_thesis: X |- p '&' q
 for r being Element of CQC-WFF A st r in {p,q} holds
X |- r by A1, A2, TARSKI:def_2;
then  X |- {p,q} by Def2;
then  X |- {(p '&' q)} by Th27, Th31;
hence  X |- p '&' q by Th10; ::_thesis: verum
end;

Lm3:  for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p '&' q holds
( X |- p & X |- q )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p '&' q holds
( X |- p & X |- q )
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p '&' q holds
( X |- p & X |- q )
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p '&' q implies ( X |- p & X |- q ) )
assume  X |- p '&' q ; ::_thesis: ( X |- p & X |- q )
then A1: X |- {(p '&' q)} by Th10;
 {p,q} |-| {(p '&' q)} by Th31;
then A2: X |- {p,q} by A1, Th27;
 p in {p,q} by TARSKI:def_2;
hence  X |- p by A2, Def2; ::_thesis: X |- q
 q in {p,q} by TARSKI:def_2;
hence  X |- q by A2, Def2; ::_thesis: verum
end;

theorem :: CQC_THE3:33
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- p '&' q iff ( X |- p & X |- q ) ) by Lm2, Lm3;

Lm4:  for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds
p '&' r |- q '&' s
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds
p '&' r |- q '&' s
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p |-| q & r |-| s implies p '&' r |- q '&' s )
assume that
A1: p |-| q and
A2: r |-| s ; ::_thesis: p '&' r |- q '&' s
 r |- s by A2, Def5;
then  {r} |- s by Def1;
then A3: {p,r} |- s by Th4, ZFMISC_1:7;
 {p,r} |-| {(p '&' r)} by Th31;
then A4: {(p '&' r)} |- {p,r} by Th18;
 p |- q by A1, Def5;
then  {p} |- q by Def1;
then  {p,r} |- q by Th4, ZFMISC_1:7;
then  {p,r} |- q '&' s by A3, Lm2;
then  {p,r} |- {(q '&' s)} by Th10;
then  {(p '&' r)} |- {(q '&' s)} by A4, Th9;
hence  p '&' r |- q '&' s by Th11; ::_thesis: verum
end;

theorem :: CQC_THE3:34
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds
p '&' r |-| q '&' s
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds
p '&' r |-| q '&' s
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p |-| q & r |-| s implies p '&' r |-| q '&' s )
assume that
A1: p |-| q and
A2: r |-| s ; ::_thesis: p '&' r |-| q '&' s
A3: q '&' s |- p '&' r by A1, A2, Lm4;
 p '&' r |- q '&' s by A1, A2, Lm4;
hence  p '&' r |-| q '&' s by A3, Def5; ::_thesis: verum
end;

theorem Th35: :: CQC_THE3:35
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A)
for x being bound_QC-variable of A holds
( X |- All (x,p) iff X |- p )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A)
for x being bound_QC-variable of A holds
( X |- All (x,p) iff X |- p )
let p be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A)
for x being bound_QC-variable of A holds
( X |- All (x,p) iff X |- p )
let X be Subset of (CQC-WFF A); ::_thesis: for x being bound_QC-variable of A holds
( X |- All (x,p) iff X |- p )
let x be bound_QC-variable of A; ::_thesis: ( X |- All (x,p) iff X |- p )
thus  ( X |- All (x,p) implies X |- p ) ::_thesis: ( X |- p implies X |- All (x,p) )
proof
A1: X |- (All (x,p)) => p by CQC_THE1:56;
assume  X |- All (x,p) ; ::_thesis: X |- p
hence  X |- p by A1, CQC_THE1:55; ::_thesis: verum
end;
thus  ( X |- p implies X |- All (x,p) ) by CQC_THE2:90; ::_thesis: verum
end;

theorem Th36: :: CQC_THE3:36
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds All (x,p) |-| p
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds All (x,p) |-| p
let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds All (x,p) |-| p
let x be bound_QC-variable of A; ::_thesis: All (x,p) |-| p
 {(All (x,p))} |- (All (x,p)) => p by CQC_THE1:56;
then  {(All (x,p))} |- p by CQC_THE1:55, CQC_THE2:87;
hence  All (x,p) |- p by Def1; :: according to CQC_THE3:def_5 ::_thesis: p |- All (x,p)
 {p} |- p by CQC_THE2:87;
then  {p} |- All (x,p) by Th35;
hence  p |- All (x,p) by Def1; ::_thesis: verum
end;

theorem :: CQC_THE3:37
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x, y being bound_QC-variable of A st p |-| q holds
All (x,p) |-| All (y,q)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x, y being bound_QC-variable of A st p |-| q holds
All (x,p) |-| All (y,q)
let p, q be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A st p |-| q holds
All (x,p) |-| All (y,q)
let x, y be bound_QC-variable of A; ::_thesis: ( p |-| q implies All (x,p) |-| All (y,q) )
assume A1: p |-| q ; ::_thesis: All (x,p) |-| All (y,q)
A2: q |-| All (y,q) by Th36;
 All (x,p) |-| p by Th36;
then  All (x,p) |-| q by A1, Th28;
hence  All (x,p) |-| All (y,q) by A2, Th28; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
predp is_an_universal_closure_of q means :Def6: :: CQC_THE3:def 6
( p is closed & ex n being Element of NAT st
( 1 <= n & ex L being FinSequence st
( len L = n & L . 1 = q & L . n = p & ( for k being Element of NAT st 1 <= k & k < n holds
ex x being bound_QC-variable of A ex r being Element of CQC-WFF A st
( r = L . k & L . (k + 1) = All (x,r) ) ) ) ) );
end;

:: deftheorem Def6 defines is_an_universal_closure_of CQC_THE3:def_6_:_
 for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p is_an_universal_closure_of q iff ( p is closed & ex n being Element of NAT st
( 1 <= n & ex L being FinSequence st
( len L = n & L . 1 = q & L . n = p & ( for k being Element of NAT st 1 <= k & k < n holds
ex x being bound_QC-variable of A ex r being Element of CQC-WFF A st
( r = L . k & L . (k + 1) = All (x,r) ) ) ) ) ) );

theorem Th38: :: CQC_THE3:38
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is_an_universal_closure_of q holds
p |-| q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is_an_universal_closure_of q holds
p |-| q
let p, q be Element of CQC-WFF A; ::_thesis: ( p is_an_universal_closure_of q implies p |-| q )
assume  p is_an_universal_closure_of q ; ::_thesis: p |-| q
then consider n being Element of NAT  such that
A1: 1 <= n and
A2: ex L being FinSequence st
( len L = n & L . 1 = q & L . n = p & ( for k being Element of NAT st 1 <= k & k < n holds
ex x being bound_QC-variable of A ex r being Element of CQC-WFF A st
( r = L . k & L . (k + 1) = All (x,r) ) ) ) by Def6;
consider L being FinSequence such that
 len L = n and
A3: L . 1 = q and
A4: L . n = p and
A5: for k being Element of NAT st 1 <= k & k < n holds
ex x being bound_QC-variable of A ex r being Element of CQC-WFF A st
( r = L . k & L . (k + 1) = All (x,r) ) by A2;
 for k being Element of NAT st 1 <= k & k <= n holds
ex r being Element of CQC-WFF A st
( r = L . k & q |-| r )
proof
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= n implies ex r being Element of CQC-WFF A st
( r = L . $1 & q |-| r ) );
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_1_<=_k_+_1_&_k_+_1_<=_n_&_not_(_k_=_0_&_ex_p,_r_being_Element_of_CQC-WFF_A_st_
(_r_=_L_._(k_+_1)_&_q_|-|_r_)_)_implies_(_1_<=_k_&_k_<_n_&_ex_s_being_Element_of_CQC-WFF_A_st_
(_s_=_L_._(k_+_1)_&_q_|-|_s_)_)_)
assume that
 1 <= k + 1 and
A8: k + 1 <= n ; ::_thesis: ( ( k = 0 & ex p, r being Element of CQC-WFF A st
( r = L . (k + 1) & q |-| r ) ) or ( 1 <= k & k < n & ex s being Element of CQC-WFF A st
( s = L . (k + 1) & q |-| s ) ) )
percases ( k = 0 or ( 1 <= k & k < n ) ) by A8, NAT_1:13, NAT_1:14;
caseA9: k = 0 ; ::_thesis: ex p, r being Element of CQC-WFF A st
( r = L . (k + 1) & q |-| r )
take p = q; ::_thesis: ex r being Element of CQC-WFF A st
( r = L . (k + 1) & q |-| r )
thus  ex r being Element of CQC-WFF A st
( r = L . (k + 1) & q |-| r ) by A3, A9; ::_thesis: verum
end;
caseA10: ( 1 <= k & k < n ) ; ::_thesis: ex s being Element of CQC-WFF A st
( s = L . (k + 1) & q |-| s )
then consider x being bound_QC-variable of A, r being Element of CQC-WFF A such that
A11: r = L . k and
A12: L . (k + 1) = All (x,r) by A5;
consider s being Element of CQC-WFF A such that
A13: s = All (x,r) ;
 s |-| r by A13, Th36;
hence  ex s being Element of CQC-WFF A st
( s = L . (k + 1) & q |-| s ) by A7, A10, A11, A12, A13, Th28; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A14: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A14, A6); ::_thesis: verum
end;
then  ex r being Element of CQC-WFF A st
( r = L . n & q |-| r ) by A1;
hence  p |-| q by A4; ::_thesis: verum
end;

theorem Th39: :: CQC_THE3:39
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p => q is valid holds
p |- q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p => q is valid holds
p |- q
let p, q be Element of CQC-WFF A; ::_thesis: ( p => q is valid implies p |- q )
assume  p => q is valid ; ::_thesis: p |- q
then  {p} |- p => q by CQC_THE1:59;
then  {p} |- q by CQC_THE1:55, CQC_THE2:87;
hence  p |- q by Def1; ::_thesis: verum
end;

theorem Th40: :: CQC_THE3:40
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => q holds
X \/ {p} |- q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => q holds
X \/ {p} |- q
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => q holds
X \/ {p} |- q
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => q implies X \/ {p} |- q )
 p in {p} by TARSKI:def_1;
then  p in X \/ {p} by XBOOLE_0:def_3;
then A1: X \/ {p} |- p by Th1;
assume  X |- p => q ; ::_thesis: X \/ {p} |- q
then  X \/ {p} |- p => q by Th4, XBOOLE_1:7;
hence  X \/ {p} |- q by A1, CQC_THE1:55; ::_thesis: verum
end;

theorem Th41: :: CQC_THE3:41
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed & p |- q holds
p => q is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is closed & p |- q holds
p => q is valid
let p, q be Element of CQC-WFF A; ::_thesis: ( p is closed & p |- q implies p => q is valid )
assume that
A1: p is closed and
A2: p |- q ; ::_thesis: p => q is valid
 ({} (CQC-WFF A)) \/ {p} |- q by A2, Def1;
then  {} (CQC-WFF A) |- p => q by A1, CQC_THE2:92;
hence  p => q is valid by CQC_THE1:def_9; ::_thesis: verum
end;

theorem :: CQC_THE3:42
for A being QC-alphabet
for p1, p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p1 is_an_universal_closure_of p holds
( X \/ {p} |- q iff X |- p1 => q )
proof
let A be QC-alphabet ; ::_thesis: for p1, p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p1 is_an_universal_closure_of p holds
( X \/ {p} |- q iff X |- p1 => q )
let p1, p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p1 is_an_universal_closure_of p holds
( X \/ {p} |- q iff X |- p1 => q )
let X be Subset of (CQC-WFF A); ::_thesis: ( p1 is_an_universal_closure_of p implies ( X \/ {p} |- q iff X |- p1 => q ) )
assume A1: p1 is_an_universal_closure_of p ; ::_thesis: ( X \/ {p} |- q iff X |- p1 => q )
now__::_thesis:_(_X_\/_{p}_|-_q_implies_X_|-_p1_=>_q_)
assume  X \/ {p} |- q ; ::_thesis: X |- p1 => q
then A2: X \/ {p} |- {q} by Th10;
 p |-| p1 by A1, Th38;
then  {p} |-| {p1} by Th29;
then  X \/ {p1} |- {q} by A2, Th26;
then A3: X \/ {p1} |- q by Th10;
 p1 is closed by A1, Def6;
hence  X |- p1 => q by A3, CQC_THE2:92; ::_thesis: verum
end;
hence  ( X \/ {p} |- q implies X |- p1 => q ) ; ::_thesis: ( X |- p1 => q implies X \/ {p} |- q )
now__::_thesis:_(_X_|-_p1_=>_q_implies_X_\/_{p}_|-_q_)
assume  X |- p1 => q ; ::_thesis: X \/ {p} |- q
then  X \/ {p1} |- q by Th40;
then A4: X \/ {p1} |- {q} by Th10;
 p |-| p1 by A1, Th38;
then  {p} |-| {p1} by Th29;
then  X \/ {p} |- {q} by A4, Th26;
hence  X \/ {p} |- q by Th10; ::_thesis: verum
end;
hence  ( X |- p1 => q implies X \/ {p} |- q ) ; ::_thesis: verum
end;

theorem Th43: :: CQC_THE3:43
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed & p |- q holds
'not' q |- 'not' p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is closed & p |- q holds
'not' q |- 'not' p
let p, q be Element of CQC-WFF A; ::_thesis: ( p is closed & p |- q implies 'not' q |- 'not' p )
assume that
A1: p is closed and
A2: p |- q ; ::_thesis: 'not' q |- 'not' p
 p => q is valid by A1, A2, Th41;
then  ('not' q) => ('not' p) is valid by LUKASI_1:52;
hence  'not' q |- 'not' p by Th39; ::_thesis: verum
end;

theorem :: CQC_THE3:44
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p is closed & X \/ {p} |- q holds
X \/ {('not' q)} |- 'not' p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p is closed & X \/ {p} |- q holds
X \/ {('not' q)} |- 'not' p
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p is closed & X \/ {p} |- q holds
X \/ {('not' q)} |- 'not' p
let X be Subset of (CQC-WFF A); ::_thesis: ( p is closed & X \/ {p} |- q implies X \/ {('not' q)} |- 'not' p )
assume that
A1: p is closed and
A2: X \/ {p} |- q ; ::_thesis: X \/ {('not' q)} |- 'not' p
 X |- p => q by A1, A2, CQC_THE2:92;
then  X |- ('not' q) => ('not' p) by LUKASI_1:69;
hence  X \/ {('not' q)} |- 'not' p by Th40; ::_thesis: verum
end;

theorem Th45: :: CQC_THE3:45
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed & 'not' p |- 'not' q holds
q |- p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is closed & 'not' p |- 'not' q holds
q |- p
let p, q be Element of CQC-WFF A; ::_thesis: ( p is closed & 'not' p |- 'not' q implies q |- p )
assume that
A1: p is closed and
A2: 'not' p |- 'not' q ; ::_thesis: q |- p
 'not' p is closed by A1, QC_LANG3:21;
then  ('not' p) => ('not' q) is valid by A2, Th41;
then  q => p is valid by LUKASI_1:52;
hence  q |- p by Th39; ::_thesis: verum
end;

theorem :: CQC_THE3:46
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p is closed & X \/ {('not' p)} |- 'not' q holds
X \/ {q} |- p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p is closed & X \/ {('not' p)} |- 'not' q holds
X \/ {q} |- p
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st p is closed & X \/ {('not' p)} |- 'not' q holds
X \/ {q} |- p
let X be Subset of (CQC-WFF A); ::_thesis: ( p is closed & X \/ {('not' p)} |- 'not' q implies X \/ {q} |- p )
assume that
A1: p is closed and
A2: X \/ {('not' p)} |- 'not' q ; ::_thesis: X \/ {q} |- p
 'not' p is closed by A1, QC_LANG3:21;
then  X |- ('not' p) => ('not' q) by A2, CQC_THE2:92;
then  X |- q => p by LUKASI_1:69;
hence  X \/ {q} |- p by Th40; ::_thesis: verum
end;

theorem :: CQC_THE3:47
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed & q is closed holds
( p |- q iff 'not' q |- 'not' p ) by Th43, Th45;

theorem Th48: :: CQC_THE3:48
for A being QC-alphabet
for p1, p, q1, q being Element of CQC-WFF A st p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q holds
( p |- q iff 'not' q1 |- 'not' p1 )
proof
let A be QC-alphabet ; ::_thesis: for p1, p, q1, q being Element of CQC-WFF A st p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q holds
( p |- q iff 'not' q1 |- 'not' p1 )
let p1, p, q1, q be Element of CQC-WFF A; ::_thesis: ( p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies ( p |- q iff 'not' q1 |- 'not' p1 ) )
assume that
A1: p1 is_an_universal_closure_of p and
A2: q1 is_an_universal_closure_of q ; ::_thesis: ( p |- q iff 'not' q1 |- 'not' p1 )
now__::_thesis:_(_p_|-_q_implies_'not'_q1_|-_'not'_p1_)
 q |-| q1 by A2, Th38;
then A3: q |- q1 by Def5;
 p1 |-| p by A1, Th38;
then A4: p1 |- p by Def5;
assume  p |- q ; ::_thesis: 'not' q1 |- 'not' p1
then  p1 |- q by A4, Th6;
then A5: p1 |- q1 by A3, Th6;
 p1 is closed by A1, Def6;
hence  'not' q1 |- 'not' p1 by A5, Th43; ::_thesis: verum
end;
hence  ( p |- q implies 'not' q1 |- 'not' p1 ) ; ::_thesis: ( 'not' q1 |- 'not' p1 implies p |- q )
now__::_thesis:_(_'not'_q1_|-_'not'_p1_implies_p_|-_q_)
 q1 |-| q by A2, Th38;
then A6: q1 |- q by Def5;
 p1 |-| p by A1, Th38;
then A7: p |- p1 by Def5;
assume A8: 'not' q1 |- 'not' p1 ; ::_thesis: p |- q
 q1 is closed by A2, Def6;
then  p1 |- q1 by A8, Th45;
then  p |- q1 by A7, Th6;
hence  p |- q by A6, Th6; ::_thesis: verum
end;
hence  ( 'not' q1 |- 'not' p1 implies p |- q ) ; ::_thesis: verum
end;

theorem :: CQC_THE3:49
for A being QC-alphabet
for p1, p, q1, q being Element of CQC-WFF A st p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q holds
( p |-| q iff 'not' p1 |-| 'not' q1 )
proof
let A be QC-alphabet ; ::_thesis: for p1, p, q1, q being Element of CQC-WFF A st p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q holds
( p |-| q iff 'not' p1 |-| 'not' q1 )
let p1, p, q1, q be Element of CQC-WFF A; ::_thesis: ( p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies ( p |-| q iff 'not' p1 |-| 'not' q1 ) )
assume that
A1: p1 is_an_universal_closure_of p and
A2: q1 is_an_universal_closure_of q ; ::_thesis: ( p |-| q iff 'not' p1 |-| 'not' q1 )
now__::_thesis:_(_p_|-|_q_implies_'not'_p1_|-|_'not'_q1_)
assume A3: p |-| q ; ::_thesis: 'not' p1 |-| 'not' q1
then  p |- q by Def5;
then A4: 'not' q1 |- 'not' p1 by A1, A2, Th48;
 q |- p by A3, Def5;
then  'not' p1 |- 'not' q1 by A1, A2, Th48;
hence  'not' p1 |-| 'not' q1 by A4, Def5; ::_thesis: verum
end;
hence  ( p |-| q implies 'not' p1 |-| 'not' q1 ) ; ::_thesis: ( 'not' p1 |-| 'not' q1 implies p |-| q )
now__::_thesis:_(_'not'_p1_|-|_'not'_q1_implies_p_|-|_q_)
assume A5: 'not' p1 |-| 'not' q1 ; ::_thesis: p |-| q
then  'not' q1 |- 'not' p1 by Def5;
then A6: p |- q by A1, A2, Th48;
 'not' p1 |- 'not' q1 by A5, Def5;
then  q |- p by A1, A2, Th48;
hence  p |-| q by A6, Def5; ::_thesis: verum
end;
hence  ( 'not' p1 |-| 'not' q1 implies p |-| q ) ; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
predp <==> q means :Def7: :: CQC_THE3:def 7
p <=> q is valid ;
reflexivity
 for p being Element of CQC-WFF A holds p <=> p is valid
proof
let p be Element of CQC-WFF A; ::_thesis: p <=> p is valid
 {} (CQC-WFF A) |- p => p by CQC_THE1:def_9;
then  {} (CQC-WFF A) |- (p => p) '&' (p => p) by Lm2;
then  (p => p) '&' (p => p) is valid by CQC_THE1:def_9;
hence  p <=> p is valid by QC_LANG2:def_4; ::_thesis: verum
end;
symmetry
 for p, q being Element of CQC-WFF A st p <=> q is valid holds
q <=> p is valid
proof
let p, q be Element of CQC-WFF A; ::_thesis: ( p <=> q is valid implies q <=> p is valid )
assume  p <=> q is valid ; ::_thesis: q <=> p is valid
then  (p => q) '&' (q => p) is valid by QC_LANG2:def_4;
then A1: {} (CQC-WFF A) |- (p => q) '&' (q => p) by CQC_THE1:def_9;
then A2: {} (CQC-WFF A) |- q => p by Lm3;
 {} (CQC-WFF A) |- p => q by A1, Lm3;
then  {} (CQC-WFF A) |- (q => p) '&' (p => q) by A2, Lm2;
then  (q => p) '&' (p => q) is valid by CQC_THE1:def_9;
hence  q <=> p is valid by QC_LANG2:def_4; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines <==> CQC_THE3:def_7_:_
 for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p <==> q iff p <=> q is valid );

theorem Th50: :: CQC_THE3:50
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p <==> q iff ( p => q is valid & q => p is valid ) )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( p <==> q iff ( p => q is valid & q => p is valid ) )
let p, q be Element of CQC-WFF A; ::_thesis: ( p <==> q iff ( p => q is valid & q => p is valid ) )
A1: now__::_thesis:_(_p_=>_q_is_valid_&_q_=>_p_is_valid_implies_p_<==>_q_)
assume that
A2: p => q is valid and
A3: q => p is valid ; ::_thesis: p <==> q
A4: {} (CQC-WFF A) |- q => p by A3, CQC_THE1:def_9;
 {} (CQC-WFF A) |- p => q by A2, CQC_THE1:def_9;
then  {} (CQC-WFF A) |- (p => q) '&' (q => p) by A4, Lm2;
then  (p => q) '&' (q => p) is valid by CQC_THE1:def_9;
then  p <=> q is valid by QC_LANG2:def_4;
hence  p <==> q by Def7; ::_thesis: verum
end;
now__::_thesis:_(_p_<==>_q_implies_(_p_=>_q_is_valid_&_q_=>_p_is_valid_)_)
assume  p <==> q ; ::_thesis: ( p => q is valid & q => p is valid )
then  p <=> q is valid by Def7;
then  (p => q) '&' (q => p) is valid by QC_LANG2:def_4;
then A5: {} (CQC-WFF A) |- (p => q) '&' (q => p) by CQC_THE1:def_9;
then A6: {} (CQC-WFF A) |- q => p by Lm3;
 {} (CQC-WFF A) |- p => q by A5, Lm3;
hence  ( p => q is valid & q => p is valid ) by A6, CQC_THE1:def_9; ::_thesis: verum
end;
hence  ( p <==> q iff ( p => q is valid & q => p is valid ) ) by A1; ::_thesis: verum
end;

theorem :: CQC_THE3:51
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p <==> q & q <==> r holds
p <==> r
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p <==> q & q <==> r holds
p <==> r
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p <==> q & q <==> r implies p <==> r )
assume that
A1: p <==> q and
A2: q <==> r ; ::_thesis: p <==> r
A3: r => q is valid by A2, Th50;
 q => p is valid by A1, Th50;
then A4: r => p is valid by A3, LUKASI_1:42;
A5: q => r is valid by A2, Th50;
 p => q is valid by A1, Th50;
then  p => r is valid by A5, LUKASI_1:42;
hence  p <==> r by A4, Th50; ::_thesis: verum
end;

theorem :: CQC_THE3:52
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <==> q holds
p |-| q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p <==> q holds
p |-| q
let p, q be Element of CQC-WFF A; ::_thesis: ( p <==> q implies p |-| q )
assume  p <==> q ; ::_thesis: p |-| q
then  p <=> q is valid by Def7;
then  (p => q) '&' (q => p) is valid by QC_LANG2:def_4;
then A1: {} (CQC-WFF A) |- (p => q) '&' (q => p) by CQC_THE1:def_9;
then  {} (CQC-WFF A) |- q => p by Lm3;
then A2: q => p is valid by CQC_THE1:def_9;
 {} (CQC-WFF A) |- p => q by A1, Lm3;
then  p => q is valid by CQC_THE1:def_9;
hence  ( p |- q & q |- p ) by A2, Th39; :: according to CQC_THE3:def_5 ::_thesis: verum
end;

Lm5:  for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <==> q holds
'not' p <==> 'not' q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p <==> q holds
'not' p <==> 'not' q
let p, q be Element of CQC-WFF A; ::_thesis: ( p <==> q implies 'not' p <==> 'not' q )
assume A1: p <==> q ; ::_thesis: 'not' p <==> 'not' q
then  q => p is valid by Th50;
then A2: ('not' p) => ('not' q) is valid by LUKASI_1:52;
 p => q is valid by A1, Th50;
then  ('not' q) => ('not' p) is valid by LUKASI_1:52;
hence  'not' p <==> 'not' q by A2, Th50; ::_thesis: verum
end;

Lm6:  for A being QC-alphabet
for p, q being Element of CQC-WFF A st 'not' p <==> 'not' q holds
p <==> q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st 'not' p <==> 'not' q holds
p <==> q
let p, q be Element of CQC-WFF A; ::_thesis: ( 'not' p <==> 'not' q implies p <==> q )
assume A1: 'not' p <==> 'not' q ; ::_thesis: p <==> q
then  ('not' q) => ('not' p) is valid by Th50;
then A2: p => q is valid by LUKASI_1:52;
 ('not' p) => ('not' q) is valid by A1, Th50;
then  q => p is valid by LUKASI_1:52;
hence  p <==> q by A2, Th50; ::_thesis: verum
end;

theorem :: CQC_THE3:53
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p <==> q iff 'not' p <==> 'not' q ) by Lm5, Lm6;

theorem Th54: :: CQC_THE3:54
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p '&' r <==> q '&' s
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p '&' r <==> q '&' s
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p <==> q & r <==> s implies p '&' r <==> q '&' s )
assume that
A1: p <==> q and
A2: r <==> s ; ::_thesis: p '&' r <==> q '&' s
 s => r is valid by A2, Th50;
then A3: s => r in TAUT A by CQC_THE1:def_10;
 q => p is valid by A1, Th50;
then  q => p in TAUT A by CQC_THE1:def_10;
then  (q '&' s) => (p '&' r) in TAUT A by A3, PROCAL_1:56;
then A4: (q '&' s) => (p '&' r) is valid by CQC_THE1:def_10;
 r => s is valid by A2, Th50;
then A5: r => s in TAUT A by CQC_THE1:def_10;
 p => q is valid by A1, Th50;
then  p => q in TAUT A by CQC_THE1:def_10;
then  (p '&' r) => (q '&' s) in TAUT A by A5, PROCAL_1:56;
then  (p '&' r) => (q '&' s) is valid by CQC_THE1:def_10;
hence  p '&' r <==> q '&' s by A4, Th50; ::_thesis: verum
end;

theorem Th55: :: CQC_THE3:55
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p => r <==> q => s
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p => r <==> q => s
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p <==> q & r <==> s implies p => r <==> q => s )
assume that
A1: p <==> q and
A2: r <==> s ; ::_thesis: p => r <==> q => s
 'not' r <==> 'not' s by A2, Lm5;
then  p '&' ('not' r) <==> q '&' ('not' s) by A1, Th54;
then A3: 'not' (p '&' ('not' r)) <==> 'not' (q '&' ('not' s)) by Lm5;
 p => r = 'not' (p '&' ('not' r)) by QC_LANG2:def_2;
hence  p => r <==> q => s by A3, QC_LANG2:def_2; ::_thesis: verum
end;

theorem :: CQC_THE3:56
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p 'or' r <==> q 'or' s
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p 'or' r <==> q 'or' s
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p <==> q & r <==> s implies p 'or' r <==> q 'or' s )
assume that
A1: p <==> q and
A2: r <==> s ; ::_thesis: p 'or' r <==> q 'or' s
 s => r is valid by A2, Th50;
then A3: s => r in TAUT A by CQC_THE1:def_10;
 q => p is valid by A1, Th50;
then  q => p in TAUT A by CQC_THE1:def_10;
then  (q 'or' s) => (p 'or' r) in TAUT A by A3, PROCAL_1:57;
then A4: (q 'or' s) => (p 'or' r) is valid by CQC_THE1:def_10;
 r => s is valid by A2, Th50;
then A5: r => s in TAUT A by CQC_THE1:def_10;
 p => q is valid by A1, Th50;
then  p => q in TAUT A by CQC_THE1:def_10;
then  (p 'or' r) => (q 'or' s) in TAUT A by A5, PROCAL_1:57;
then  (p 'or' r) => (q 'or' s) is valid by CQC_THE1:def_10;
hence  p 'or' r <==> q 'or' s by A4, Th50; ::_thesis: verum
end;

theorem :: CQC_THE3:57
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p <=> r <==> q <=> s
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p <=> r <==> q <=> s
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p <==> q & r <==> s implies p <=> r <==> q <=> s )
assume that
A1: p <==> q and
A2: r <==> s ; ::_thesis: p <=> r <==> q <=> s
A3: r => p <==> s => q by A1, A2, Th55;
A4: p <=> r = (p => r) '&' (r => p) by QC_LANG2:def_4;
 p => r <==> q => s by A1, A2, Th55;
then  (p => r) '&' (r => p) <==> (q => s) '&' (s => q) by A3, Th54;
hence  p <=> r <==> q <=> s by A4, QC_LANG2:def_4; ::_thesis: verum
end;

theorem Th58: :: CQC_THE3:58
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
All (x,p) <==> All (x,q)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
All (x,p) <==> All (x,q)
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p <==> q holds
All (x,p) <==> All (x,q)
let x be bound_QC-variable of A; ::_thesis: ( p <==> q implies All (x,p) <==> All (x,q) )
assume A1: p <==> q ; ::_thesis: All (x,p) <==> All (x,q)
then  q => p is valid by Th50;
then  All (x,(q => p)) is valid by CQC_THE2:23;
then A2: (All (x,q)) => (All (x,p)) is valid by CQC_THE2:31;
 p => q is valid by A1, Th50;
then  All (x,(p => q)) is valid by CQC_THE2:23;
then  (All (x,p)) => (All (x,q)) is valid by CQC_THE2:31;
hence  All (x,p) <==> All (x,q) by A2, Th50; ::_thesis: verum
end;

theorem :: CQC_THE3:59
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
Ex (x,p) <==> Ex (x,q)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
Ex (x,p) <==> Ex (x,q)
let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p <==> q holds
Ex (x,p) <==> Ex (x,q)
let x be bound_QC-variable of A; ::_thesis: ( p <==> q implies Ex (x,p) <==> Ex (x,q) )
assume  p <==> q ; ::_thesis: Ex (x,p) <==> Ex (x,q)
then  'not' p <==> 'not' q by Lm5;
then  All (x,('not' p)) <==> All (x,('not' q)) by Th58;
then A1: 'not' (All (x,('not' p))) <==> 'not' (All (x,('not' q))) by Lm5;
 Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def_5;
hence  Ex (x,p) <==> Ex (x,q) by A1, QC_LANG2:def_5; ::_thesis: verum
end;

theorem Th60: :: CQC_THE3:60
for A being QC-alphabet
for k being Element of NAT
for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let k be Element of NAT ; ::_thesis: for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let l be QC-variable_list of k,A; ::_thesis: for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let a be free_QC-variable of A; ::_thesis: for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let x be bound_QC-variable of A; ::_thesis: still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
now__::_thesis:_for_y_being_set_st_y_in_still_not-bound_in_l_holds_
y_in_still_not-bound_in_(Subst_(l,(a_.-->_x)))
let y be set ; ::_thesis: ( y in still_not-bound_in l implies y in still_not-bound_in (Subst (l,(a .--> x))) )
A1: still_not-bound_in l =  {  (l . n) where n is Element of NAT : ( 1 <= n & n <= len l & l . n in bound_QC-variables A )  }  by QC_LANG1:def_29;
assume A2: y in still_not-bound_in l ; ::_thesis: y in still_not-bound_in (Subst (l,(a .--> x)))
then reconsider y9 = y as Element of still_not-bound_in l ;
A3: still_not-bound_in (Subst (l,(a .--> x))) =  {  ((Subst (l,(a .--> x))) . n) where n is Element of NAT : ( 1 <= n & n <= len (Subst (l,(a .--> x))) & (Subst (l,(a .--> x))) . n in bound_QC-variables A )  }  by QC_LANG1:def_29;
consider n being Element of NAT  such that
A4: y9 = l . n and
A5: 1 <= n and
A6: n <= len l and
A7: l . n in bound_QC-variables A by A1, A2;
 l . n <> a by A7, QC_LANG3:34;
then A8: l . n = (Subst (l,(a .--> x))) . n by A5, A6, CQC_LANG:3;
 n <= len (Subst (l,(a .--> x))) by A6, CQC_LANG:def_1;
hence  y in still_not-bound_in (Subst (l,(a .--> x))) by A3, A4, A5, A7, A8; ::_thesis: verum
end;
hence  still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x))) by TARSKI:def_3; ::_thesis: verum
end;

theorem Th61: :: CQC_THE3:61
for A being QC-alphabet
for k being Element of NAT
for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let k be Element of NAT ; ::_thesis: for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let l be QC-variable_list of k,A; ::_thesis: for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let a be free_QC-variable of A; ::_thesis: for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let x be bound_QC-variable of A; ::_thesis: still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in still_not-bound_in (Subst (l,(a .--> x))) or y in (still_not-bound_in l) \/ {x} )
A1: still_not-bound_in l =  {  (l . n) where n is Element of NAT : ( 1 <= n & n <= len l & l . n in bound_QC-variables A )  }  by QC_LANG1:def_29;
assume A2: y in still_not-bound_in (Subst (l,(a .--> x))) ; ::_thesis: y in (still_not-bound_in l) \/ {x}
then reconsider y9 = y as Element of still_not-bound_in (Subst (l,(a .--> x))) ;
 still_not-bound_in (Subst (l,(a .--> x))) =  {  ((Subst (l,(a .--> x))) . n) where n is Element of NAT : ( 1 <= n & n <= len (Subst (l,(a .--> x))) & (Subst (l,(a .--> x))) . n in bound_QC-variables A )  }  by QC_LANG1:def_29;
then consider n being Element of NAT  such that
A3: y9 = (Subst (l,(a .--> x))) . n and
A4: 1 <= n and
A5: n <= len (Subst (l,(a .--> x))) and
A6: (Subst (l,(a .--> x))) . n in bound_QC-variables A by A2;
A7: n <= len l by A5, CQC_LANG:def_1;
percases ( l . n = a or l . n <> a ) ;
suppose l . n = a ; ::_thesis: y in (still_not-bound_in l) \/ {x}
then  y9 = x by A3, A4, A7, CQC_LANG:3;
then  y9 in {x} by TARSKI:def_1;
hence  y in (still_not-bound_in l) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose l . n <> a ; ::_thesis: y in (still_not-bound_in l) \/ {x}
then  l . n = (Subst (l,(a .--> x))) . n by A4, A7, CQC_LANG:3;
then  y9 in still_not-bound_in l by A1, A3, A4, A6, A7;
hence  y in (still_not-bound_in l) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;

theorem Th62: :: CQC_THE3:62
for A being QC-alphabet
for x being bound_QC-variable of A
for h being QC-formula of A holds still_not-bound_in h c= still_not-bound_in (h . x)
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for h being QC-formula of A holds still_not-bound_in h c= still_not-bound_in (h . x)
let x be bound_QC-variable of A; ::_thesis: for h being QC-formula of A holds still_not-bound_in h c= still_not-bound_in (h . x)
defpred S1[ QC-formula of A] means  still_not-bound_in $1 c= still_not-bound_in ($1 . x);
A1: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p]
proof
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ 'not' p] )
still_not-bound_in (('not' p) . x) = still_not-bound_in ('not' (p . x)) by CQC_LANG:19
.= still_not-bound_in (p . x) by QC_LANG3:7 ;
hence  ( S1[p] implies S1[ 'not' p] ) by QC_LANG3:7; ::_thesis: verum
end;
A2: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF A; ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume that
A3: S1[p] and
A4: S1[q] ; ::_thesis: S1[p '&' q]
A5: still_not-bound_in ((p '&' q) . x) = still_not-bound_in ((p . x) '&' (q . x)) by CQC_LANG:21
.= (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) by QC_LANG3:10 ;
 still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG3:10;
hence  S1[p '&' q] by A3, A4, A5, XBOOLE_1:13; ::_thesis: verum
end;
A6: for x being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (x,p)]
proof
let y be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ All (y,p)] )
assume A7: S1[p] ; ::_thesis: S1[ All (y,p)]
percases ( y = x or y <> x ) ;
suppose y = x ; ::_thesis: S1[ All (y,p)]
hence  S1[ All (y,p)] by CQC_LANG:24; ::_thesis: verum
end;
supposeA8: y <> x ; ::_thesis: S1[ All (y,p)]
A9: still_not-bound_in (All (y,p)) = (still_not-bound_in p) \ {y} by QC_LANG3:12;
still_not-bound_in ((All (y,p)) . x) = still_not-bound_in (All (y,(p . x))) by A8, CQC_LANG:25
.= (still_not-bound_in (p . x)) \ {y} by QC_LANG3:12 ;
hence  S1[ All (y,p)] by A7, A9, XBOOLE_1:33; ::_thesis: verum
end;
end;
end;
A10: for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[P ! ll]
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[P ! ll]
let P be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds S1[P ! ll]
let ll be QC-variable_list of k,A; ::_thesis: S1[P ! ll]
A11: still_not-bound_in ((P ! ll) . x) = still_not-bound_in (P ! (Subst (ll,((A a. 0) .--> x)))) by CQC_LANG:17
.= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by QC_LANG3:5 ;
 still_not-bound_in ll c= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by Th60;
hence  S1[P ! ll] by A11, QC_LANG3:5; ::_thesis: verum
end;
A12: S1[ VERUM A] by CQC_LANG:15;
thus  for h being QC-formula of A holds S1[h] from QC_LANG1:sch_1(A10, A12, A1, A2, A6); ::_thesis: verum
end;

theorem Th63: :: CQC_THE3:63
for A being QC-alphabet
for x being bound_QC-variable of A
for h being QC-formula of A holds still_not-bound_in (h . x) c= (still_not-bound_in h) \/ {x}
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for h being QC-formula of A holds still_not-bound_in (h . x) c= (still_not-bound_in h) \/ {x}
let x be bound_QC-variable of A; ::_thesis: for h being QC-formula of A holds still_not-bound_in (h . x) c= (still_not-bound_in h) \/ {x}
defpred S1[ QC-formula of A] means  still_not-bound_in ($1 . x) c= (still_not-bound_in $1) \/ {x};
A1: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p]
proof
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ 'not' p] )
still_not-bound_in (('not' p) . x) = still_not-bound_in ('not' (p . x)) by CQC_LANG:19
.= still_not-bound_in (p . x) by QC_LANG3:7 ;
hence  ( S1[p] implies S1[ 'not' p] ) by QC_LANG3:7; ::_thesis: verum
end;
A2: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF A; ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume that
A3: S1[p] and
A4: S1[q] ; ::_thesis: S1[p '&' q]
A5: still_not-bound_in ((p '&' q) . x) = still_not-bound_in ((p . x) '&' (q . x)) by CQC_LANG:21
.= (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) by QC_LANG3:10 ;
A6: ((still_not-bound_in p) \/ {x}) \/ ((still_not-bound_in q) \/ {x}) = ((still_not-bound_in p) \/ ({x} \/ (still_not-bound_in q))) \/ {x} by XBOOLE_1:4
.= (((still_not-bound_in p) \/ (still_not-bound_in q)) \/ {x}) \/ {x} by XBOOLE_1:4
.= ((still_not-bound_in p) \/ (still_not-bound_in q)) \/ ({x} \/ {x}) by XBOOLE_1:4
.= ((still_not-bound_in p) \/ (still_not-bound_in q)) \/ {x} ;
 (still_not-bound_in (p . x)) \/ (still_not-bound_in (q . x)) c= ((still_not-bound_in p) \/ {x}) \/ ((still_not-bound_in q) \/ {x}) by A3, A4, XBOOLE_1:13;
hence  S1[p '&' q] by A5, A6, QC_LANG3:10; ::_thesis: verum
end;
A7: for x being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (x,p)]
proof
let y be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ All (y,p)] )
assume A8: S1[p] ; ::_thesis: S1[ All (y,p)]
percases ( y = x or y <> x ) ;
supposeA9: y = x ; ::_thesis: S1[ All (y,p)]
A10: (still_not-bound_in p) \ {x} c= still_not-bound_in p by XBOOLE_1:36;
A11: still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} by QC_LANG3:12;
 still_not-bound_in p c= still_not-bound_in (p . x) by Th62;
then  still_not-bound_in (All (x,p)) c= still_not-bound_in (p . x) by A11, A10, XBOOLE_1:1;
then A12: still_not-bound_in (All (x,p)) c= (still_not-bound_in p) \/ {x} by A8, XBOOLE_1:1;
(still_not-bound_in (All (y,p))) \/ {x} = ((still_not-bound_in p) \ {x}) \/ {x} by A9, QC_LANG3:12
.= (still_not-bound_in p) \/ {x} by XBOOLE_1:39 ;
hence  S1[ All (y,p)] by A9, A12, CQC_LANG:24; ::_thesis: verum
end;
supposeA13: y <> x ; ::_thesis: S1[ All (y,p)]
A14: (still_not-bound_in (All (y,p))) \/ {x} = ((still_not-bound_in p) \ {y}) \/ {x} by QC_LANG3:12
.= ((still_not-bound_in p) \/ {x}) \ {y} by A13, XBOOLE_1:87, ZFMISC_1:11 ;
still_not-bound_in ((All (y,p)) . x) = still_not-bound_in (All (y,(p . x))) by A13, CQC_LANG:25
.= (still_not-bound_in (p . x)) \ {y} by QC_LANG3:12 ;
hence  S1[ All (y,p)] by A8, A14, XBOOLE_1:33; ::_thesis: verum
end;
end;
end;
A15: for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[P ! ll]
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[P ! ll]
let P be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds S1[P ! ll]
let ll be QC-variable_list of k,A; ::_thesis: S1[P ! ll]
A16: still_not-bound_in ((P ! ll) . x) = still_not-bound_in (P ! (Subst (ll,((A a. 0) .--> x)))) by CQC_LANG:17
.= still_not-bound_in (Subst (ll,((A a. 0) .--> x))) by QC_LANG3:5 ;
 still_not-bound_in (Subst (ll,((A a. 0) .--> x))) c= (still_not-bound_in ll) \/ {x} by Th61;
hence  S1[P ! ll] by A16, QC_LANG3:5; ::_thesis: verum
end;
A17: still_not-bound_in (VERUM A) = {} by QC_LANG3:3;
 (VERUM A) . x = VERUM A by CQC_LANG:15;
then  still_not-bound_in ((VERUM A) . x) = {} by A17;
then A18: still_not-bound_in ((VERUM A) . x) c= (still_not-bound_in (VERUM A)) \/ {x} by XBOOLE_1:2;
A19: S1[ VERUM A] by A18;
thus  for h being QC-formula of A holds S1[h] from QC_LANG1:sch_1(A15, A19, A1, A2, A7); ::_thesis: verum
end;

theorem Th64: :: CQC_THE3:64
for A being QC-alphabet
for p being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p
let p be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p
let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p
let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & x <> y & not y in still_not-bound_in h implies not y in still_not-bound_in p )
assume that
A1: p = h . x and
A2: x <> y and
A3: not y in still_not-bound_in h and
A4: y in still_not-bound_in p ; ::_thesis: contradiction
A5: still_not-bound_in p c= (still_not-bound_in h) \/ {x} by A1, Th63;
percases ( y in still_not-bound_in h or y in {x} ) by A4, A5, XBOOLE_0:def_3;
suppose y in still_not-bound_in h ; ::_thesis: contradiction
hence  contradiction by A3; ::_thesis: verum
end;
suppose y in {x} ; ::_thesis: contradiction
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
end;
end;

theorem :: CQC_THE3:65
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)
let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)
let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)
let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h implies All (x,p) <==> All (y,q) )
assume that
A1: p = h . x and
A2: q = h . y and
A3: not x in still_not-bound_in h and
A4: not y in still_not-bound_in h ; ::_thesis: All (x,p) <==> All (y,q)
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: All (x,p) <==> All (y,q)
hence  All (x,p) <==> All (y,q) by A1, A2; ::_thesis: verum
end;
supposeA5: x <> y ; ::_thesis: All (x,p) <==> All (y,q)
then  not x in still_not-bound_in q by A2, A3, Th64;
then A6: (All (y,q)) => (All (x,p)) is valid by A1, A2, A4, CQC_THE2:27;
 not y in still_not-bound_in p by A1, A4, A5, Th64;
then  (All (x,p)) => (All (y,q)) is valid by A1, A2, A3, CQC_THE2:27;
hence  All (x,p) <==> All (y,q) by A6, Th50; ::_thesis: verum
end;
end;
end;