consider X being set such that

A1: for x being set holds

( x in X iff ( x in the carrier of L & S_{1}[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

A1: for x being set holds

( x in X iff ( x in the carrier of L & S

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