defpred S₁[ set ] means the Source of G . $1 = x;
consider X being set such that
A8: for z being set holds
( z in X iff ( z in the carrier' of G & S₁[z] ) ) from XBOOLE_0:sch 1();
for z being set st z in X holds
z in the carrier' of G by A8;
then X c= the carrier' of G by TARSKI:def 3;
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 Source 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 Source 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 Source of G . z = x ) ) ) & card X = card X ) by A8; :: thesis: verum