defpred S₁[ set ] means card $1 = 2;
consider X being Subset of G such that
A1: for x being set holds
( x in X iff ( x in G & S₁[x] ) ) from SUBSET_1:sch 1();
take X ; :: thesis: for e being set holds
( e in X iff ( e in G & card e = 2 ) )
thus for e being set holds
( e in X iff ( e in G & card e = 2 ) ) by A1; :: thesis: verum