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