set LS = LeastSort t;
set PTA = ParsedTermsOSA X;
reconsider x1 = t as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort t) by Def12;
let O1, O2 be Element of OSClass R,(LeastSort t); :: thesis: ( ( for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
O1 = OSClass R,x ) & ( for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
O2 = OSClass R,x ) implies O1 = O2 )
assume that
A2: for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
O1 = OSClass R,x and
A3: for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
O2 = OSClass R,x ; :: thesis: O1 = O2
thus O1 = OSClass R,x1 by A2
.= O2 by A3 ; :: thesis: verum