let L be complete sup-Semilattice; :: thesis: for S being non empty full join-inheriting SubRelStr of L st Bottom L in the carrier of S holds

for X being Subset of L

for Y being Subset of S st X = Y holds

finsups Y c= finsups X

let S be non empty full join-inheriting SubRelStr of L; :: thesis: ( Bottom L in the carrier of S implies for X being Subset of L

for Y being Subset of S st X = Y holds

finsups Y c= finsups X )

assume A1: Bottom L in the carrier of S ; :: thesis: for X being Subset of L

for Y being Subset of S st X = Y holds

finsups Y c= finsups X

let X be Subset of L; :: thesis: for Y being Subset of S st X = Y holds

finsups Y c= finsups X

let Y be Subset of S; :: thesis: ( X = Y implies finsups Y c= finsups X )

assume A2: X = Y ; :: thesis: finsups Y c= finsups X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in finsups Y or x in finsups X )

assume x in finsups Y ; :: thesis: x in finsups X

then x in { ("\/" (V,S)) where V is finite Subset of Y : ex_sup_of V,S } by WAYBEL_0:def 27;

then consider Z being finite Subset of Y such that

A3: x = "\/" (Z,S) and

A4: ex_sup_of Z,S ;

reconsider Z = Z as finite Subset of X by A2;

for X being Subset of L

for Y being Subset of S st X = Y holds

finsups Y c= finsups X

let S be non empty full join-inheriting SubRelStr of L; :: thesis: ( Bottom L in the carrier of S implies for X being Subset of L

for Y being Subset of S st X = Y holds

finsups Y c= finsups X )

assume A1: Bottom L in the carrier of S ; :: thesis: for X being Subset of L

for Y being Subset of S st X = Y holds

finsups Y c= finsups X

let X be Subset of L; :: thesis: for Y being Subset of S st X = Y holds

finsups Y c= finsups X

let Y be Subset of S; :: thesis: ( X = Y implies finsups Y c= finsups X )

assume A2: X = Y ; :: thesis: finsups Y c= finsups X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in finsups Y or x in finsups X )

assume x in finsups Y ; :: thesis: x in finsups X

then x in { ("\/" (V,S)) where V is finite Subset of Y : ex_sup_of V,S } by WAYBEL_0:def 27;

then consider Z being finite Subset of Y such that

A3: x = "\/" (Z,S) and

A4: ex_sup_of Z,S ;

reconsider Z = Z as finite Subset of X by A2;

now :: thesis: x in finsups Xend;

hence
x in finsups X
; :: thesis: verumper cases
( not Z is empty or Z is empty )
;

end;

suppose
not Z is empty
; :: thesis: x in finsups X

then reconsider Z1 = Z as non empty finite Subset of S by XBOOLE_1:1;

reconsider xl = "\/" (Z1,L) as Element of S by WAYBEL21:15;

A5: ex_sup_of Z1,L by YELLOW_0:17;

xl is_>=_than Z1

then x in { ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L } by A3, A5;

hence x in finsups X by WAYBEL_0:def 27; :: thesis: verum

end;reconsider xl = "\/" (Z1,L) as Element of S by WAYBEL21:15;

A5: ex_sup_of Z1,L by YELLOW_0:17;

A6: now :: thesis: for b being Element of S st b is_>=_than Z1 holds

xl <= b

A8:
"\/" (Z1,L) is_>=_than Z1
by A5, YELLOW_0:30;xl <= b

let b be Element of S; :: thesis: ( b is_>=_than Z1 implies xl <= b )

reconsider b1 = b as Element of L by YELLOW_0:58;

assume A7: b is_>=_than Z1 ; :: thesis: xl <= b

b1 is_>=_than Z1 by A7, YELLOW_0:59;

then "\/" (Z1,L) <= b1 by A5, YELLOW_0:30;

hence xl <= b by YELLOW_0:60; :: thesis: verum

end;reconsider b1 = b as Element of L by YELLOW_0:58;

assume A7: b is_>=_than Z1 ; :: thesis: xl <= b

b1 is_>=_than Z1 by A7, YELLOW_0:59;

then "\/" (Z1,L) <= b1 by A5, YELLOW_0:30;

hence xl <= b by YELLOW_0:60; :: thesis: verum

xl is_>=_than Z1

proof

then
"\/" (Z1,S) = "\/" (Z1,L)
by A6, YELLOW_0:30;
let b be Element of S; :: according to LATTICE3:def 9 :: thesis: ( not b in Z1 or b <= xl )

reconsider b1 = b as Element of L by YELLOW_0:58;

assume b in Z1 ; :: thesis: b <= xl

then b1 <= "\/" (Z1,L) by A8;

hence b <= xl by YELLOW_0:60; :: thesis: verum

end;reconsider b1 = b as Element of L by YELLOW_0:58;

assume b in Z1 ; :: thesis: b <= xl

then b1 <= "\/" (Z1,L) by A8;

hence b <= xl by YELLOW_0:60; :: thesis: verum

then x in { ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L } by A3, A5;

hence x in finsups X by WAYBEL_0:def 27; :: thesis: verum

suppose A9:
Z is empty
; :: thesis: x in finsups X

reconsider dL = Bottom L as Element of S by A1;

reconsider dS = Bottom S as Element of L by YELLOW_0:58;

S is lower-bounded by A4, A9, WAYBEL20:6;

then Bottom S <= dL by YELLOW_0:44;

then A10: dS <= Bottom L by YELLOW_0:59;

A11: ex_sup_of Z,L by YELLOW_0:17;

Bottom L <= dS by YELLOW_0:44;

then dS = Bottom L by A10, YELLOW_0:def 3;

then x in { ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L } by A3, A9, A11;

hence x in finsups X by WAYBEL_0:def 27; :: thesis: verum

end;reconsider dS = Bottom S as Element of L by YELLOW_0:58;

S is lower-bounded by A4, A9, WAYBEL20:6;

then Bottom S <= dL by YELLOW_0:44;

then A10: dS <= Bottom L by YELLOW_0:59;

A11: ex_sup_of Z,L by YELLOW_0:17;

Bottom L <= dS by YELLOW_0:44;

then dS = Bottom L by A10, YELLOW_0:def 3;

then x in { ("\/" (V,L)) where V is finite Subset of X : ex_sup_of V,L } by A3, A9, A11;

hence x in finsups X by WAYBEL_0:def 27; :: thesis: verum