QC-symbols A c= QC-symbols A ;
then reconsider symb = QC-symbols A as non empty Subset of (QC-symbols A) ;
set z = min symb;
take min symb ; :: thesis: for t being QC-symbol of A holds min symb <= t
thus for t being QC-symbol of A holds min symb <= t by Def35; :: thesis: verum