let L be non empty Poset; 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; 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; ( ( 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
; SupBelow (R,C) is sup-closed
let X be Subset of (SupBelow (R,C)); WAYBEL35:def 9 ( ex_sup_of X,L implies "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) )
set s = "\/" (X,L);
assume A2:
ex_sup_of X,L
; "\/" (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;
LATTICE3:def 9 ( 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
;
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;
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; verum