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 )
(PTMin X) . t2 in OSClass (PTCongruence X),t2 by Th41;
then A1: OSClass (PTCongruence X),t2 = OSClass (PTCongruence X),((PTMin X) . t2) by Th35;
(PTMin X) . t1 in OSClass (PTCongruence X),t1 by Th41;
then A2: OSClass (PTCongruence X),t1 = OSClass (PTCongruence X),((PTMin X) . t1) by Th35;
assume (PTMin X) . t2 = (PTMin X) . t1 ; :: thesis: t2 in OSClass (PTCongruence X),t1
hence t2 in OSClass (PTCongruence X),t1 by A2, A1, Th33; :: thesis: verum