set t = the Element of TS (DTConOSA X);
take (PTMin X) . the Element of TS (DTConOSA X) ; :: thesis: (PTMin X) . ((PTMin X) . the Element of TS (DTConOSA X)) = (PTMin X) . the Element of TS (DTConOSA X)
thus (PTMin X) . ((PTMin X) . the Element of TS (DTConOSA X)) = (PTMin X) . the Element of TS (DTConOSA X) by Th43; :: thesis: verum