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 ;
hence x <= sup (SetBelow (R,C,("\/" (X,L)))) by ; :: thesis: verum
end;
then A7: "\/" (X,L) <= sup (SetBelow (R,C,("\/" (X,L)))) by ;
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 ;
then "\/" (X,L) = sup (SetBelow (R,C,("\/" (X,L)))) by ;
then "\/" (X,L) in SupBelow (R,C) by Def10;
hence "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) by ; :: thesis: verum