take {(id the set )} ; :: thesis: ( {(id the set )} is composition-closed & {(id the set )} is inverse-closed & not {(id the set )} is empty )
thus ( {(id the set )} is composition-closed & {(id the set )} is inverse-closed & not {(id the set )} is empty ) ; :: thesis: verum