let L be RelStr ; 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; for C being set
for y being Element of L holds SetBelow (R,C,y) is_<=_than y
let C be set ; for y being Element of L holds SetBelow (R,C,y) is_<=_than y
let y be Element of L; SetBelow (R,C,y) is_<=_than y
let b be Element of L; LATTICE3:def 9 ( not b in SetBelow (R,C,y) or b <= y )
assume
b in SetBelow (R,C,y)
; b <= y
then
[b,y] in R
by Th15;
hence
b <= y
by WAYBEL_4:def 3; verum