let X be non empty constituted-DTrees set ; :: thesis: Subtrees X = union { (Subtrees t) where t is Element of X : verum }
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (Subtrees t) where t is Element of X : verum } c= Subtrees X
let x be object ; :: thesis: ( x in Subtrees X implies x in union { (Subtrees s) where s is Element of X : verum } )
assume x in Subtrees X ; :: thesis: x in union { (Subtrees s) where s is Element of X : verum }
then consider t being Element of X such that
A1: ex p being Node of t st x = t | p ;
( Subtrees t in { (Subtrees s) where s is Element of X : verum } & x in Subtrees t ) by A1;
hence x in union { (Subtrees s) where s is Element of X : verum } by TARSKI:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (Subtrees t) where t is Element of X : verum } or x in Subtrees X )
assume x in union { (Subtrees s) where s is Element of X : verum } ; :: thesis: x in Subtrees X
then consider Y being set such that
A2: x in Y and
A3: Y in { (Subtrees s) where s is Element of X : verum } by TARSKI:def 4;
consider t being Element of X such that
A4: Y = Subtrees t by A3;
ex p being Node of t st x = t | p by A2, A4;
hence x in Subtrees X ; :: thesis: verum