defpred S₁[ 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₁[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 ) )

hereby :: thesis: ( 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;

thus ( ex y being Element of L st
( y <= x & y in X ) implies x in S ) by A6; :: thesis: verum