let X be set ; :: thesis: ( X is S -mincover implies X is S -covering )
assume B0: X is S -mincover ; :: thesis: X is S -covering
thus for phi being wff string of S st not phi in X holds
xnot phi in X by B0, DefCover; :: according to FOMODEL2:def 40 :: thesis: verum
thus verum ; :: thesis: verum