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