reconsider t = bool GRZ-formula-set as Subset-Family of GRZ-formula-set ;
take t ; :: thesis: not t is empty
thus not t is empty by ZFMISC_1:def 1; :: thesis: verum