thus ( F is non-void-yielding implies for i being set st i in rng F holds
i is non void TopStruct ) by Def13, Def14; :: thesis: ( ( for i being set st i in rng F holds
i is non void TopStruct ) implies F is non-void-yielding )
assume A1: for i being set st i in rng F holds
i is non void TopStruct ; :: thesis: F is non-void-yielding
let S be TopStruct ; :: according to PENCIL_1:def 14 :: thesis: ( S in rng F implies not S is void )
thus ( S in rng F implies not S is void ) by A1; :: thesis: verum