defpred S₁[ object ] means 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 ( a . i <> 1_ G & i in I ) )
thus for i being object holds
( i in X iff ( a . i <> 1_ G & i in I ) ) by A1; :: thesis: verum