let C be strict_chain of R; ( C is trivial implies C is satisfying_SIC )
assume A1:
C is trivial
; C is satisfying_SIC
let x, z be Element of L; WAYBEL35:def 6,WAYBEL35:def 7 ( x in C & z in C & [x,z] in R & x <> z implies ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y ) )
assume that
A2:
x in C
and
A3:
z in C
and
[x,z] in R
and
A4:
x <> z
; ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
thus
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
by A2, A3, A4, A1, SUBSET_1:def 7; verum