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))))

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

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

then A7:
"\/" (X,L) <= sup (SetBelow (R,C,("\/" (X,L))))
by A2, YELLOW_0:def 9;
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;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

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