defpred S_{1}[ object ] means ex c1 being Element of L st

( c1 = $1 & a <= c1 & c1 <= b );

consider S being set such that

A1: for c being object holds

( c in S iff ( c in the carrier of L & S_{1}[c] ) )
from XBOOLE_0:sch 1();

for c being object 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

( c1 = $1 & a <= c1 & c1 <= b );

consider S being set such that

A1: for c being object holds

( c in S iff ( c in the carrier of L & S

for c being object 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 )

end;thus ( c in S implies ( a <= c & c <= b ) ) :: thesis: ( a <= c & c <= b implies c in S )

proof

thus
( a <= c & c <= b implies c in S )
by A1; :: thesis: verum
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;then ex c1 being Element of L st

( c1 = c & a <= c1 & c1 <= b ) by A1;

hence ( a <= c & c <= b ) ; :: thesis: verum