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
A1: 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 A1;
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 A1;
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 A1; :: thesis: verum