for X being set st X <> {} holds
{ x where x is Element of X : verum } = X by Lm72;