let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for t1 being Element of TS (DTConOSA X) holds (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1
let X be non-empty ManySortedSet of S; :: thesis: for t1 being Element of TS (DTConOSA X) holds (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1
let t1 be Element of TS (DTConOSA X); :: thesis: (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1
(PTMin X) . t1 in OSClass ((PTCongruence X),t1) by Th40;
hence (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1 by Th42; :: thesis: verum