let z be set ; :: thesis: for C being initialized ConstructorSignature holds
( z is quasi-type of C iff ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st z = [A,q] )
let C be initialized ConstructorSignature; :: thesis: ( z is quasi-type of C iff ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st z = [A,q] )
( z in QuasiTypes C iff ex t being expression of C, a_Type C ex A being finite Subset of (QuasiAdjs C) st
( z = [A,t] & t is pure ) ) ;
hence ( z is quasi-type of C iff ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st z = [A,q] ) by Def43; :: thesis: verum