set X = GRZ-formula-set ;
GRZ-formula-set c= GRZ-formula-set ;
then reconsider X = GRZ-formula-set as Subset of GRZ-formula-set ;
take X ; :: thesis: not X is empty
thus not X is empty ; :: thesis: verum