let S be OrderSortedSign; :: thesis: for X being OrderSortedSet of S holds OSCl X = X
let X be OrderSortedSet of S; :: thesis: OSCl X = X
( X c= OSCl X & OSCl X c= X ) by Th7, Th8;
hence OSCl X = X by PBOOLE:146; :: thesis: verum