consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool the carrier of L & S₁[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