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