set t = the Element of the generators of G . s;
( the generators of G . s c= the Sorts of T . s & the Element of the generators of G . s in the generators of G . s ) by PBOOLE:def 2, PBOOLE:def 18;
hence ex b₁ being Element of T,s st b₁ in the generators of G . s ; :: thesis: verum