thus ( Y is non empty Subset of (QC-symbols A) implies the Element of Y is QC-symbol of A ) :: thesis: ( Y is not non empty Subset of (QC-symbols A) implies 0 A is QC-symbol of A )

proof

assume A1: Y is non empty Subset of (QC-symbols A) ; :: thesis: the Element of Y is QC-symbol of A
consider a being set such that
A2: a = the Element of Y ;
A3: a in Y by A1, A2;
a is QC-symbol of A by A1, A3;
hence the Element of Y is QC-symbol of A by A2; :: thesis: verum

end;

thus ( Y is not non empty Subset of (QC-symbols A) implies 0 A is QC-symbol of A ) ; :: thesis: verum