defpred S1[ 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 & S1[x] ) )
from XBOOLE_0:sch 1();
S c= the carrier of L
by A6;
then reconsider S = S as Subset of L ;
take
S
; 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; ( x in S iff ex y being Element of L st
( y <= x & y in X ) )
hereby ( ex y being Element of L st
( y <= x & y in X ) implies x in S )
assume
x in S
;
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 )
;
verum
end;
thus
( ex y being Element of L st
( y <= x & y in X ) implies x in S )
by A6; verum