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 ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st [x,y] = [A,q] by Th72;
hence ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C ) by XTUPLE_0:1; :: 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 Th72; :: thesis: verum