let S be locally_directed OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
for s being Element of S
for t being Element of TS (DTConOSA X)
for x, x1 being set st x in X . s & t = root-tree [x,s] holds
( x1 in OSClass (LCongruence X),t iff x1 = t )
let X be V5() ManySortedSet of ; :: thesis: for s being Element of S
for t being Element of TS (DTConOSA X)
for x, x1 being set st x in X . s & t = root-tree [x,s] holds
( x1 in OSClass (LCongruence X),t iff x1 = t )
let s be Element of S; :: thesis: for t being Element of TS (DTConOSA X)
for x, x1 being set st x in X . s & t = root-tree [x,s] holds
( x1 in OSClass (LCongruence X),t iff x1 = t )
let t be Element of TS (DTConOSA X); :: thesis: for x, x1 being set st x in X . s & t = root-tree [x,s] holds
( x1 in OSClass (LCongruence X),t iff x1 = t )
set R = LCongruence X;
set R1 = PTCongruence X;
LCongruence X c= PTCongruence X by Def18;
then A1: OSClass (LCongruence X),t c= OSClass (PTCongruence X),t by Th36;
let x, x1 be set ; :: thesis: ( x in X . s & t = root-tree [x,s] implies ( x1 in OSClass (LCongruence X),t iff x1 = t ) )
assume A2: ( x in X . s & t = root-tree [x,s] ) ; :: thesis: ( x1 in OSClass (LCongruence X),t iff x1 = t )
thus ( x1 in OSClass (LCongruence X),t implies x1 = t ) by A1, A2, Th34; :: thesis: ( x1 = t implies x1 in OSClass (LCongruence X),t )
assume x1 = t ; :: thesis: x1 in OSClass (LCongruence X),t
hence x1 in OSClass (LCongruence X),t by Th33; :: thesis: verum