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