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 ( 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 )
then consider y being Element of L such that
A2: y in C and
A3: [x,y] in R and
A4: [y,z] in R and
A5: x <> y by A1, Def6;
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 A2, A3, A4; :: thesis: x < y
x <= y by A3, WAYBEL_4:def 4;
hence x < y by A5, ORDERS_2:def 10; :: thesis: verum