defpred S_{1}[ object ] means ex a, y being Element of L st

( a = $1 & y <= a & y in X );

consider S being set such that

A6: for x being object holds

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

S c= the carrier of L by A6;

then reconsider S = S as Subset of L ;

take S ; :: thesis: for x being Element of L holds

( x in S iff ex y being Element of L st

( y <= x & y in X ) )

let x be Element of L; :: thesis: ( x in S iff ex y being Element of L st

( y <= x & y in X ) )

( y <= x & y in X ) implies x in S ) by A6; :: thesis: verum

( a = $1 & y <= a & y in X );

consider S being set such that

A6: for x being object holds

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

S c= the carrier of L by A6;

then reconsider S = S as Subset of L ;

take S ; :: thesis: for x being Element of L holds

( x in S iff ex y being Element of L st

( y <= x & y in X ) )

let x be Element of L; :: thesis: ( x in S iff ex y being Element of L st

( y <= x & y in X ) )

hereby :: thesis: ( ex y being Element of L st

( y <= x & y in X ) implies x in S )

thus
( ex y being Element of L st ( y <= x & y in X ) implies x in S )

assume
x in S
; :: thesis: ex y being Element of L st

( y <= x & y in X )

then ex a, y being Element of L st

( a = x & y <= a & y in X ) by A6;

hence ex y being Element of L st

( y <= x & y in X ) ; :: thesis: verum

end;( y <= x & y in X )

then ex a, y being Element of L st

( a = x & y <= a & y in X ) by A6;

hence ex y being Element of L st

( y <= x & y in X ) ; :: thesis: verum

( y <= x & y in X ) implies x in S ) by A6; :: thesis: verum