let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is expression of C, an_Adj C : a is regular } or x in Union the Sorts of (Free C,(MSVars C)) )
assume x in { a where a is expression of C, an_Adj C : a is regular } ; :: thesis: x in Union the Sorts of (Free C,(MSVars C))
then ex a being expression of C, an_Adj C st
( x = a & a is regular ) ;
hence x in Union the Sorts of (Free C,(MSVars C)) ; :: thesis: verum