let G be strict Group; :: thesis: for a being Element of G holds
( a in Phi G iff not a is generating )
let a be Element of G; :: thesis: ( a in Phi G iff not a is generating )
thus ( a in Phi G implies not a is generating ) :: thesis: ( not a is generating implies a in Phi G )
proof
assume a in Phi G ; :: thesis: not a is generating
then a in the carrier of (Phi G) by STRUCT_0:def 5;
then a in { b where b is Element of G : not b is generating } by Th41;
then ex b being Element of G st
( a = b & not b is generating ) ;
hence not a is generating ; :: thesis: verum
end;
assume not a is generating ; :: thesis: a in Phi G
then a in { b where b is Element of G : not b is generating } ;
then a in the carrier of (Phi G) by Th41;
hence a in Phi G by STRUCT_0:def 5; :: thesis: verum