let L be RelStr ; :: thesis: for R being auxiliary(i) Relation of L
for C being set
for y being Element of L holds SetBelow R,C,y is_<=_than y
let R be auxiliary(i) Relation of L; :: thesis: for C being set
for y being Element of L holds SetBelow R,C,y is_<=_than y
let C be set ; :: thesis: for y being Element of L holds SetBelow R,C,y is_<=_than y
let y be Element of L; :: thesis: SetBelow R,C,y is_<=_than y
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in SetBelow R,C,y or b <= y )
assume b in SetBelow R,C,y ; :: thesis: b <= y
then [b,y] in R by Th18;
hence b <= y by WAYBEL_4:def 4; :: thesis: verum