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