let A be QC-alphabet ; for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
let S be Element of QC-Sub-WFF A; ( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
thus
( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 )
( ( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
thus
( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A )
( ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )proof
assume
S is
Sub_atomic
;
ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A
then consider k being
Nat,
P being
QC-pred_symbol of
k,
A,
ll being
QC-variable_list of
k,
A,
e being
Element of
vSUB A such that A1:
S = Sub_P (
P,
ll,
e)
;
S = [(P ! ll),e]
by A1, Th9;
then
S `1 = P ! ll
;
then
@ (S `1) = <*P*> ^ ll
by QC_LANG1:8;
then
(@ (S `1)) . 1
= P
by FINSEQ_1:41;
hence
ex
k being
Nat st
(@ (S `1)) . 1 is
QC-pred_symbol of
k,
A
;
verum
end;
thus
( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 )
( ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
thus
( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 )
( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 )
thus
( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 )
verum