let S be Element of QC-Sub-WFF ; :: 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, ll being QC-variable_list of k, e being Element of vSUB 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 16; :: thesis: verum