let x, y be set ; :: thesis: for C being initialized ConstructorSignature holds
( [x,y] is quasi-type of C iff ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C ) )
let C be initialized ConstructorSignature; :: thesis: ( [x,y] is quasi-type of C iff ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C ) )

hereby :: thesis: ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C implies [x,y] is quasi-type of C )

assume [x,y] is quasi-type of C ; :: thesis: ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C )
then consider A being finite Subset of (QuasiAdjs C), q being pure expression of C, a_Type C such that
A1: [x,y] = [A,q] by Th54;
thus ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C ) by A1, ZFMISC_1:33; :: thesis: verum

end;

thus ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C implies [x,y] is quasi-type of C ) by Th54; :: thesis: verum