let t be DecoratedTree; :: thesis: for n being Node of t holds Subtrees (t | n) c= Subtrees t
let n be Node of t; :: thesis: Subtrees (t | n) c= Subtrees t
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Subtrees (t | n) or x in Subtrees t )
assume x in Subtrees (t | n) ; :: thesis: x in Subtrees t
then consider p being Node of (t | n) such that
A1: x = (t | n) | p ;
dom (t | n) = (dom t) | n by TREES_2:def 11;
then reconsider q = n ^ p as Node of t by TREES_1:def 9;
x = t | q by A1, Th3;
hence x in Subtrees t ; :: thesis: verum