let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for t being Term of S,X
for x being set st x in Subtrees t holds
x is Term of S,X
let X be non-empty ManySortedSet of S; :: thesis: for t being Term of S,X
for x being set st x in Subtrees t holds
x is Term of S,X
let t be Term of S,X; :: thesis: for x being set st x in Subtrees t holds
x is Term of S,X
let x be set ; :: thesis: ( x in Subtrees t implies x is Term of S,X )
assume x in Subtrees t ; :: thesis: x is Term of S,X
then consider p being Element of dom t such that
A1: x = t | p ;
thus x is Term of S,X by A1; :: thesis: verum