defpred S₁[ set ] means $1 = sup (SetBelow R,C,$1);
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of L & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for y being set holds
( y in X iff y = sup (SetBelow R,C,y) )
thus for y being set holds
( y in X iff y = sup (SetBelow R,C,y) ) by A1; :: thesis: verum