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

proof

let a be Element of L; :: thesis: ( SetBelow (R,C,x) is_<=_than a implies x <= a )
assume A5: SetBelow (R,C,x) is_<=_than a ; :: thesis: x <= a
x in SetBelow (R,C,x) by A1, A2, Th18;
hence x <= a by A5, LATTICE3:def 9; :: thesis: verum

end;

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