let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being V2() ManySortedSet of S holds LCongruence X = PTCongruence X
let X be V2() 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