set D = DTConOSA X;
set F = PTClasses X;
let R1, R2 be MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X; :: thesis: ( ( for i being set st i in the carrier of S holds
R1 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) & ( for i being set st i in the carrier of S holds
R2 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) implies R1 = R2 )
assume that
A28: for i being set st i in the carrier of S holds
R1 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } and
A29: for i being set st i in the carrier of S holds
R2 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ; :: thesis: R1 = R2

now

let i be set ; :: thesis: ( i in the carrier of S implies R1 . i = R2 . i )
assume A30: i in the carrier of S ; :: thesis: R1 . i = R2 . i
( R1 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } & R2 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) by A28, A29, A30;
hence R1 . i = R2 . i ; :: thesis: verum

end;

hence R1 = R2 by PBOOLE:3; :: thesis: verum