let A be QC-alphabet ; :: thesis: ( not A is empty & A is Relation-like )
ex X being set st
( NAT c= X & A = [:NAT,X:] ) by Def1;
hence ( not A is empty & A is Relation-like ) by Def1; :: thesis: verum