let D be non empty set ; :: thesis: FinTrees D c= Trees D
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in FinTrees D or x in Trees D )
thus ( not x in FinTrees D or x in Trees D ) by Def7; :: thesis: verum