defpred S₁[ set ] means ex a, b being Point of st
( $1 = [a,b] & b <= (2 * a) - 1 );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of [:I[01] ,I[01] :] & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= the carrier of [:I[01] ,I[01] :]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in the carrier of [:I[01] ,I[01] :] )
assume x in X ; :: thesis: x in the carrier of [:I[01] ,I[01] :]
hence x in the carrier of [:I[01] ,I[01] :] by A1; :: thesis: verum

end;

then reconsider X = X as Subset of ;
take X ; :: thesis: for x being set holds
( x in X iff ex a, b being Point of st
( x = [a,b] & b <= (2 * a) - 1 ) )
thus for x being set holds
( x in X iff ex a, b being Point of st
( x = [a,b] & b <= (2 * a) - 1 ) ) by A1; :: thesis: verum