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_{1} being Element of T,s st b_{1} in the generators of G . s
; :: thesis: verum

( 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