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