defpred S₁[ object ] means ex a, b being Point of I[01] st
( $1 = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 );
consider X being set such that
A1: for x being object 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]:] by A1;
then reconsider X = X as Subset of [:I[01],I[01]:] ;
take X ; :: thesis: for x being set holds
( x in X iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) )
thus for x being set holds
( x in X iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) by A1; :: thesis: verum