set v = the positive expression of C, an_Adj C;
the positive expression of C, an_Adj C in { a where a is expression of C, an_Adj C : a is regular } ;
hence not QuasiAdjs C is empty ; :: thesis: QuasiAdjs C is constituted-DTrees
let x be object ; :: according to TREES_3:def 5 :: thesis: ( not x in QuasiAdjs C or x is set )
assume x in QuasiAdjs C ; :: thesis: x is set
hence x is set ; :: thesis: verum