(* PLUS-ITERATED SUPCLOSURE *************************************************)
-(* Main propertis ***********************************************************)
+(* Main properties **********************************************************)
theorem fqup_trans: tri_transitive … fqup.
/2 width=5 by tri_TC_transitive/ qed-.