consider X being set such that

A1: for x being set holds

( x in X iff ( x in bool the carrier of L & S_{1}[x] ) )
from XFAMILY:sch 1();

take X ; :: thesis: for x being set holds

( x in X iff ( x is strict_chain of R & C c= x ) )

thus for x being set holds

( x in X iff ( x is strict_chain of R & C c= x ) ) by A1; :: thesis: verum

A1: for x being set holds

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

take X ; :: thesis: for x being set holds

( x in X iff ( x is strict_chain of R & C c= x ) )

thus for x being set holds

( x in X iff ( x is strict_chain of R & C c= x ) ) by A1; :: thesis: verum