let L be non empty Poset; :: thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being Subset of L st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds
SupBelow (R,C) is sup-closed
let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: for C being Subset of L st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds
SupBelow (R,C) is sup-closed
let C be Subset of L; :: thesis: ( ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) implies SupBelow (R,C) is sup-closed )
assume A1: for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ; :: thesis: SupBelow (R,C) is sup-closed
let X be Subset of (SupBelow (R,C)); :: according to WAYBEL35:def 9 :: thesis: ( ex_sup_of X,L implies "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) )
set s = "\/" (X,L);
assume A2: ex_sup_of X,L ; :: thesis: "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C))))
A3: ex_sup_of SetBelow (R,C,("\/" (X,L))),L by A1;
X is_<=_than sup (SetBelow (R,C,("\/" (X,L))))

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= sup (SetBelow (R,C,("\/" (X,L)))) )
A4: ex_sup_of SetBelow (R,C,x),L by A1;
assume A5: x in X ; :: thesis: x <= sup (SetBelow (R,C,("\/" (X,L))))
then A6: x = sup (SetBelow (R,C,x)) by Def10;
SetBelow (R,C,x) c= SetBelow (R,C,("\/" (X,L))) by A2, A5, Th17, YELLOW_4:1;
hence x <= sup (SetBelow (R,C,("\/" (X,L)))) by A3, A6, A4, YELLOW_0:34; :: thesis: verum

end;

then A7: "\/" (X,L) <= sup (SetBelow (R,C,("\/" (X,L)))) by A2, YELLOW_0:def 9;
A8: the carrier of (subrelstr (SupBelow (R,C))) = SupBelow (R,C) by YELLOW_0:def 15;
SetBelow (R,C,("\/" (X,L))) is_<=_than "\/" (X,L) by Th16;
then sup (SetBelow (R,C,("\/" (X,L)))) <= "\/" (X,L) by A3, YELLOW_0:def 9;
then "\/" (X,L) = sup (SetBelow (R,C,("\/" (X,L)))) by A7, ORDERS_2:2;
then "\/" (X,L) in SupBelow (R,C) by Def10;
hence "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) by A8, A2, YELLOW_0:64; :: thesis: verum