let S be locally_directed OrderSortedSign; for X being V2() 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 V2() 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 s be 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 t be 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 )
set R = LCongruence X;
set R1 = PTCongruence X;
let x, x1 be set ; ( 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]
; ( 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; ( x1 = t implies x1 in OSClass ((LCongruence X),t) )
assume
x1 = t
; x1 in OSClass ((LCongruence X),t)
hence
x1 in OSClass ((LCongruence X),t)
by Th32; verum