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 that
A2: x in C and
A3: z in C and
[x,z] in R and
A4: x <> z ; :: thesis: 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; :: thesis: verum