let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being V5 ManySortedSet of S
for t1, t2 being Element of TS (DTConOSA X) holds
( t2 in OSClass (PTCongruence X),t1 iff (PTMin X) . t2 = (PTMin X) . t1 )
let X be V5 ManySortedSet of S; :: thesis: for t1, t2 being Element of TS (DTConOSA X) holds
( t2 in OSClass (PTCongruence X),t1 iff (PTMin X) . t2 = (PTMin X) . t1 )
let t1, t2 be Element of TS (DTConOSA X); :: thesis: ( t2 in OSClass (PTCongruence X),t1 iff (PTMin X) . t2 = (PTMin X) . t1 )
set R = PTCongruence X;
set M = PTMin X;
thus ( t2 in OSClass (PTCongruence X),t1 implies (PTMin X) . t2 = (PTMin X) . t1 ) by Th42; :: thesis: ( (PTMin X) . t2 = (PTMin X) . t1 implies t2 in OSClass (PTCongruence X),t1 )
assume A1: (PTMin X) . t2 = (PTMin X) . t1 ; :: thesis: t2 in OSClass (PTCongruence X),t1
( (PTMin X) . t2 in OSClass (PTCongruence X),t2 & (PTMin X) . t1 in OSClass (PTCongruence X),t1 ) by Th41;
then ( OSClass (PTCongruence X),t1 = OSClass (PTCongruence X),((PTMin X) . t1) & OSClass (PTCongruence X),t2 = OSClass (PTCongruence X),((PTMin X) . t2) ) by Th35;
hence t2 in OSClass (PTCongruence X),t1 by A1, Th33; :: thesis: verum