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 Th15;
hence b <= y by WAYBEL_4:def 3; :: thesis: verum