let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of
for s being SortSymbol of S holds FreeGen s,X = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }
let X be V5() ManySortedSet of ; :: thesis: for s being SortSymbol of S holds FreeGen s,X = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }
let s be SortSymbol of S; :: thesis: FreeGen s,X = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }
set D = DTConMSA X;
set A = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ;
thus FreeGen s,X c= { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } :: according to XBOOLE_0:def 10 :: thesis: { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } c= FreeGen s,X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in FreeGen s,X or x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } )
assume x in FreeGen s,X ; :: thesis: x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }
then consider a being set such that
A1: ( a in X . s & x = root-tree [a,s] ) by Def17;
A2: [a,s] in Terminals (DTConMSA X) by A1, Th7;
then reconsider t = [a,s] as Symbol of (DTConMSA X) ;
t `2 = s by MCART_1:7;
hence x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by A1, A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } or x in FreeGen s,X )
assume x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ; :: thesis: x in FreeGen s,X
then consider t being Symbol of (DTConMSA X) such that
A3: ( x = root-tree t & t in Terminals (DTConMSA X) & t `2 = s ) ;
consider s1 being SortSymbol of S, a being set such that
A4: ( a in X . s1 & t = [a,s1] ) by A3, Th7;
s = s1 by A3, A4, MCART_1:7;
hence x in FreeGen s,X by A3, A4, Def17; :: thesis: verum