set S = { [p,(t | p)] where p is Node of t : verum } ;
{ [p,(t | p)] where p is Node of t : verum } c= [:(dom t),(Subtrees t):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [p,(t | p)] where p is Node of t : verum } or x in [:(dom t),(Subtrees t):] )
assume x in { [p,(t | p)] where p is Node of t : verum } ; :: thesis: x in [:(dom t),(Subtrees t):]
then consider p being Node of t such that
A1: x = [p,(t | p)] ;
t | p in Subtrees t ;
hence x in [:(dom t),(Subtrees t):] by A1, ZFMISC_1:87; :: thesis: verum
end;
hence { [p,(t | p)] where p is Node of t : verum } is Subset of [:(dom t),(Subtrees t):] ; :: thesis: verum