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