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