take W = SymmetricHull L; :: thesis: ( W is total & W is reflexive & W is symmetric )
thus ( W is total & W is reflexive & W is symmetric ) ; :: thesis: verum