let S be locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
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 non-empty ManySortedSet of S; :: 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;
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 that
A1: x in X . s and
A2: t = root-tree [x,s] ; :: thesis: ( x1 in OSClass ((LCongruence X),t) iff x1 = t )
LCongruence X c= PTCongruence X by Def17;
then OSClass ((LCongruence X),t) c= OSClass ((PTCongruence X),t) by Th35;
hence ( x1 in OSClass ((LCongruence X),t) implies x1 = t ) by A1, A2, Th33; :: 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 Th32; :: thesis: verum