defpred S₁[ set ] means ex c1 being Element of L st
( c1 = $1 & a <= c1 & c1 <= b );
consider S being set such that
A1: for c being set holds
( c in S iff ( c in the carrier of L & S₁[c] ) ) from XBOOLE_0:sch 1();
for c being set st c in S holds
c in the carrier of L by A1;
then reconsider S = S as Subset of L by TARSKI:def 3;
reconsider S = S as Subset of L ;
take S ; :: thesis: for c being Element of L holds
( c in S iff ( a <= c & c <= b ) )
thus for c being Element of L holds
( c in S iff ( a <= c & c <= b ) ) :: thesis: verum

proof

let c be Element of L; :: thesis: ( c in S iff ( a <= c & c <= b ) )
thus ( c in S implies ( a <= c & c <= b ) ) :: thesis: ( a <= c & c <= b implies c in S )

proof

assume c in S ; :: thesis: ( a <= c & c <= b )
then ex c1 being Element of L st
( c1 = c & a <= c1 & c1 <= b ) by A1;
hence ( a <= c & c <= b ) ; :: thesis: verum

end;

thus ( a <= c & c <= b implies c in S ) by A1; :: thesis: verum

end;