let L be RelStr ; :: thesis: for R being auxiliary(i) Relation of L

for C being set

for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds

x = sup (SetBelow (R,C,x))

let R be auxiliary(i) Relation of L; :: thesis: for C being set

for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds

x = sup (SetBelow (R,C,x))

let C be set ; :: thesis: for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds

x = sup (SetBelow (R,C,x))

let x be Element of L; :: thesis: ( x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L implies x = sup (SetBelow (R,C,x)) )

assume that

A1: x in C and

A2: [x,x] in R and

A3: ex_sup_of SetBelow (R,C,x),L ; :: thesis: x = sup (SetBelow (R,C,x))

A4: for a being Element of L st SetBelow (R,C,x) is_<=_than a holds

x <= a by A1, A2, Th15;

SetBelow (R,C,x) is_<=_than x by Th16;

hence x = sup (SetBelow (R,C,x)) by A4, A3, YELLOW_0:def 9; :: thesis: verum

for C being set

for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds

x = sup (SetBelow (R,C,x))

let R be auxiliary(i) Relation of L; :: thesis: for C being set

for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds

x = sup (SetBelow (R,C,x))

let C be set ; :: thesis: for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds

x = sup (SetBelow (R,C,x))

let x be Element of L; :: thesis: ( x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L implies x = sup (SetBelow (R,C,x)) )

assume that

A1: x in C and

A2: [x,x] in R and

A3: ex_sup_of SetBelow (R,C,x),L ; :: thesis: x = sup (SetBelow (R,C,x))

A4: for a being Element of L st SetBelow (R,C,x) is_<=_than a holds

x <= a by A1, A2, Th15;

SetBelow (R,C,x) is_<=_than x by Th16;

hence x = sup (SetBelow (R,C,x)) by A4, A3, YELLOW_0:def 9; :: thesis: verum