let A be QC-alphabet ; for x being bound_QC-variable of A
for p being Element of QC-WFF A st Free p = {} holds
p . x = p
let x be bound_QC-variable of A; for p being Element of QC-WFF A st Free p = {} holds
p . x = p
let p be Element of QC-WFF A; ( Free p = {} implies p . x = p )
defpred S1[ Element of QC-WFF A] means ( Free $1 = {} implies $1 . x = $1 );
A1:
for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p]
by Th19, QC_LANG3:55;
A2:
for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
A4:
for k being Nat
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds S1[P ! l]
A8:
for y being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
proof
let y be
bound_QC-variable of
A;
for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]let p be
Element of
QC-WFF A;
( S1[p] implies S1[ All (y,p)] )
assume A9:
(
Free p = {} implies
p . x = p )
;
S1[ All (y,p)]
A10:
(
x = y implies
(All (y,p)) . x = All (
y,
p) )
by Th24;
assume
Free (All (y,p)) = {}
;
(All (y,p)) . x = All (y,p)
hence
(All (y,p)) . x = All (
y,
p)
by A9, A10, Th25, QC_LANG3:58;
verum
end;
A11:
S1[ VERUM A]
by Th15;
for p being Element of QC-WFF A holds S1[p]
from QC_LANG1:sch 1(A4, A11, A1, A2, A8);
hence
( Free p = {} implies p . x = p )
; verum