let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being V16() ManySortedSet of S holds LCongruence X = PTCongruence X
let X be V16() ManySortedSet of S; :: thesis: LCongruence X = PTCongruence X
A1: PTCongruence X c= LCongruence X by Th46;
LCongruence X c= PTCongruence X by Def18;
hence LCongruence X = PTCongruence X by A1, PBOOLE:def 10; :: thesis: verum