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 XFAMILY: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