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, Th20, 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 Th19;
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:25;
then "\/" X,L in SupBelow R,C by Def10;
hence "\/" X,L = "\/" X,(subrelstr (SupBelow R,C)) by A8, A2, YELLOW_0:65; :: thesis: verum