let s2, s3 be SortSymbol of S; :: thesis: ( t in the Sorts of (ParsedTermsOSA X) . s2 & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s2 <= s1 ) & t in the Sorts of (ParsedTermsOSA X) . s3 & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s3 <= s1 ) implies s2 = s3 )
assume that
A7: t in the Sorts of (ParsedTermsOSA X) . s2 and
A8: for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s2 <= s1 and
A9: t in the Sorts of (ParsedTermsOSA X) . s3 and
A10: for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s3 <= s1 ; :: thesis: s2 = s3
A11: s2 <= s3 by A8, A9;
s3 <= s2 by A7, A10;
hence s2 = s3 by A11, ORDERS_2:2; :: thesis: verum