let S be OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for s being Element of S
for x being set st x in X . s holds
for t being Element of TS (DTConOSA X) st t = root-tree [x,s] holds
LeastSort t = s
let X be non-empty ManySortedSet of S; :: thesis: for s being Element of S
for x being set st x in X . s holds
for t being Element of TS (DTConOSA X) st t = root-tree [x,s] holds
LeastSort t = s
let s be Element of S; :: thesis: for x being set st x in X . s holds
for t being Element of TS (DTConOSA X) st t = root-tree [x,s] holds
LeastSort t = s
let x be set ; :: thesis: ( x in X . s implies for t being Element of TS (DTConOSA X) st t = root-tree [x,s] holds
LeastSort t = s )
assume A1: x in X . s ; :: thesis: for t being Element of TS (DTConOSA X) st t = root-tree [x,s] holds
LeastSort t = s
reconsider s2 = s as Element of S ;
let t be Element of TS (DTConOSA X); :: thesis: ( t = root-tree [x,s] implies LeastSort t = s )
assume A2: t = root-tree [x,s] ; :: thesis: LeastSort t = s
A3: for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s2 <= s1 by A1, A2, Th10;
t in the Sorts of (ParsedTermsOSA X) . s2 by A1, A2, Th10;
hence LeastSort t = s by A3, Def12; :: thesis: verum