set x = the Element of (FreeGen T) . s;
( the Element of (FreeGen T) . s in (FreeGen T) . s & (FreeGen T) . s c= G . s ) by Def3, PBOOLE:def 2;
then reconsider x = the Element of (FreeGen T) . s as Element of G . s ;
take x ; :: thesis: x is pure
thus x in (FreeGen T) . s ; :: according to AOFA_A01:def 4 :: thesis: verum