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 A7, WAYBEL_4:def 3;

hence x < y by A9, ORDERS_2:def 6; :: thesis: verum

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 A7, WAYBEL_4:def 3;

hence x < y by A9, ORDERS_2:def 6; :: thesis: verum