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 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 ;
hence S `1 is atomic ; :: thesis: verum