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;
A2: the carrier of (subrelstr (SupBelow R,C)) = SupBelow R,C by YELLOW_0:def 15;
assume A3: ex_sup_of X,L ; :: thesis: "\/" X,L = "\/" X,(subrelstr (SupBelow R,C))
A4: ex_sup_of SetBelow R,C,("\/" X,L),L by A1;
SetBelow R,C,("\/" X,L) is_<=_than "\/" X,L by Th19;
then A5: sup (SetBelow R,C,("\/" X,L)) <= "\/" X,L by A4, YELLOW_0:def 9;
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)) )
assume A6: x in X ; :: thesis: x <= sup (SetBelow R,C,("\/" X,L))
then A7: x = sup (SetBelow R,C,x) by Def10;
A8: ex_sup_of SetBelow R,C,x,L by A1;
SetBelow R,C,x c= SetBelow R,C,("\/" X,L) by A3, A6, Th20, YELLOW_4:1;
hence x <= sup (SetBelow R,C,("\/" X,L)) by A4, A7, A8, YELLOW_0:34; :: thesis: verum

end;

then "\/" X,L <= sup (SetBelow R,C,("\/" X,L)) by A3, YELLOW_0:def 9;
then "\/" X,L = sup (SetBelow R,C,("\/" X,L)) by A5, ORDERS_2:25;
then A9: "\/" X,L in SupBelow R,C by Def10;
thus "\/" X,L = "\/" X,(subrelstr (SupBelow R,C)) by A2, A3, A9, YELLOW_0:65; :: thesis: verum