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

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