let L be RelStr ; :: thesis: for C being set
for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds
for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y )

let C be set ; :: thesis: for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds
for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y )

let R be auxiliary(i) Relation of L; :: thesis: ( R satisfies_SIC_on C implies for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y ) )

assume A1: R satisfies_SIC_on C ; :: thesis: for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y )

let x, z be Element of L; :: 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
A4: [x,z] in R and
A5: x <> z ; :: thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y )

consider y being Element of L such that
A6: y in C and
A7: [x,y] in R and
A8: [y,z] in R and
A9: x <> y by A2, A3, A4, A5, A1;
take y ; :: thesis: ( y in C & [x,y] in R & [y,z] in R & x < y )
thus ( y in C & [x,y] in R & [y,z] in R ) by A6, A7, A8; :: thesis: x < y
x <= y by ;
hence x < y by ; :: thesis: verum