let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being non-empty 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 non-empty 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 Th41; :: thesis: ( (PTMin X) . t2 = (PTMin X) . t1 implies t2 in OSClass ((PTCongruence X),t1) )
(PTMin X) . t2 in OSClass ((PTCongruence X),t2) by Th40;
then A1: OSClass ((PTCongruence X),t2) = OSClass ((PTCongruence X),((PTMin X) . t2)) by Th34;
(PTMin X) . t1 in OSClass ((PTCongruence X),t1) by Th40;
then A2: OSClass ((PTCongruence X),t1) = OSClass ((PTCongruence X),((PTMin X) . t1)) by Th34;
assume (PTMin X) . t2 = (PTMin X) . t1 ; :: thesis: t2 in OSClass ((PTCongruence X),t1)
hence t2 in OSClass ((PTCongruence X),t1) by A2, A1, Th32; :: thesis: verum