let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S holds LCongruence X = PTCongruence X
let X be non-empty ManySortedSet of S; :: thesis: LCongruence X = PTCongruence X
A1: PTCongruence X c= LCongruence X by Th45;
LCongruence X c= PTCongruence X by Def17;
hence LCongruence X = PTCongruence X by A1, PBOOLE:146; :: thesis: verum