ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st T = [A,q] by Th72;
hence the_base_of is pure expression of C, a_Type C ; :: thesis: verum