let X, Y be set ; :: thesis: ( X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees )
assume A1: for x being set st x in X holds
x is finite Tree ; :: according to TREES_3:def 4 :: thesis: ( not Y c= X or Y is constituted-FinTrees )
assume A2: Y c= X ; :: thesis: Y is constituted-FinTrees
let x be set ; :: according to TREES_3:def 4 :: thesis: ( x in Y implies x is finite Tree )
assume x in Y ; :: thesis: x is finite Tree
hence x is finite Tree by A1, A2; :: thesis: verum