let x be object ; :: 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