(* STAR-ITERATED SUPCLOSURE *************************************************)
-(* Advaveded properties *****************************************************)
+(* Main properties **********************************************************)
theorem fqus_trans: tri_transitive … fqus.
/2 width=5 by tri_TC_transitive/ qed-.