thus not QuasiTerms C is empty ; :: thesis: QuasiTerms C is constituted-DTrees
let x be set ; :: according to TREES_3:def 5 :: thesis: ( not x in QuasiTerms C or x is set )
assume x in QuasiTerms C ; :: thesis: x is set
hence x is set ; :: thesis: verum