let x be quasi-type of C; :: thesis: x is pair
ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st x = [A,q] by Th72;
hence x is pair ; :: thesis: verum