let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
S `1 is atomic
let S be Element of QC-Sub-WFF A; :: thesis: ( S is Sub_atomic implies S `1 is atomic )
assume S is Sub_atomic ; :: thesis: S `1 is atomic
then consider k being Element of 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) by Def25;
S = [(P ! ll),e] by A1, Th9;
then S `1 = P ! ll by MCART_1:7;
hence S `1 is atomic by QC_LANG1:def 18; :: thesis: verum