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