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