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

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