let C be strict_chain of R; :: thesis: ( C is trivial implies C is satisfying_SIC )
assume A1: C is trivial ; :: thesis: C is satisfying_SIC
let x, z be Element of L; :: according to WAYBEL35:def 6,WAYBEL35:def 7 :: thesis: ( 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 ( x in C & z in C & [x,z] in R & x <> z ) ; :: thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
hence ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y ) by A1, YELLOW_8:def 1; :: thesis: verum