set p0 = the Node of t;
set S = { [p,(t | p)] where p is Node of t : verum } ;
[ the Node of t,(t | the Node of t)] in { [p,(t | p)] where p is Node of t : verum } ;
hence not FixedSubtrees t is empty ; :: thesis: verum