defpred S₁[ object ] means ex G being Group st
( G = F . $1 & a . $1 <> 1_ G );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in I & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being object st x in X holds
x in I by A1;
then reconsider X = X as Subset of I by TARSKI:def 3;
take X ; :: thesis: for i being object holds
( i in X iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) )
let i be object ; :: thesis: ( i in X iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) )
thus ( i in X implies ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) ) :: thesis: ( ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) implies i in X )

proof

assume A2: i in X ; :: thesis: ex G being Group st
( G = F . i & a . i <> 1_ G & i in I )
then ex G being Group st
( G = F . i & a . i <> 1_ G ) by A1;
hence ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) by A2; :: thesis: verum

end;

thus ( ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) implies i in X ) by A1; :: thesis: verum