consider t being Element of TS (DTConOSA X);
take (PTMin X) . t ; :: thesis: (PTMin X) . ((PTMin X) . t) = (PTMin X) . t
thus (PTMin X) . ((PTMin X) . t) = (PTMin X) . t by Th44; :: thesis: verum