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 & [x,x] in R ) and
A2: ex_sup_of SetBelow R,C,x,L ; :: thesis: x = sup (SetBelow R,C,x)
A3: SetBelow R,C,x is_<=_than x by Th19;
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 A4: SetBelow R,C,x is_<=_than a ; :: thesis: x <= a
x in SetBelow R,C,x by A1, Th18;
hence x <= a by A4, LATTICE3:def 9; :: thesis: verum

end;

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