theorem Th73: :: ABCMIZ_1:73

for x, y being set
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 ) )