defpred S₁[ object ] means the Target of G . $1 = x;
consider X being set such that
A1: for z being object holds
( z in X iff ( z in the carrier' of G & S₁[z] ) ) from XBOOLE_0:sch 1();
for z being object st z in X holds
z in the carrier' of G by A1;
then X c= the carrier' of G ;
then reconsider X = X as finite set ;
take card X ; :: thesis: ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & card X = card X )
take X ; :: thesis: ( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & card X = card X )
thus ( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & card X = card X ) by A1; :: thesis: verum