the carrier of U0 c= the carrier of U0 ;
then reconsider GG = the carrier of U0 as non empty Subset of U0 ;
take GG ; :: thesis: for A being Subset of U0 st A is opers_closed & GG c= A holds
A = the carrier of U0
thus for A being Subset of U0 st A is opers_closed & GG c= A holds
A = the carrier of U0 ; :: thesis: verum