theorem :: LUKASI_1:43

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is valid holds
q => p is valid by Th13;