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
A1: t in the Sorts of (ParsedTermsOSA X) . s2 and
A2: for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s2 <= s1 and
A3: t in the Sorts of (ParsedTermsOSA X) . s3 and
A4: for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s3 <= s1 ; :: thesis: s2 = s3
A5: s2 <= s3 by A2, A3;
s3 <= s2 by A1, A4;
hence s2 = s3 by A5, ORDERS_2:2; :: thesis: verum