let z be set ; :: thesis: for C being initialized ConstructorSignature holds
( z is quasi-adjective of C iff z in QuasiAdjs C )
let C be initialized ConstructorSignature; :: thesis: ( z is quasi-adjective of C iff z in QuasiAdjs C )
( z in QuasiAdjs C iff ex a being expression of C, an_Adj C st
( z = a & a is regular ) ) ;
hence ( z is quasi-adjective of C iff z in QuasiAdjs C ) ; :: thesis: verum