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 set ; :: 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

per cases ( not Z is empty or Z is empty ) ;

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;
A5: ex_sup_of Z1,L by YELLOW_0:17;
reconsider xl = "\/" Z1,L as Element of S by WAYBEL21:15;
A6: ( "\/" Z1,L is_>=_than Z1 & ( for b being Element of L st b is_>=_than Z1 holds
"\/" Z1,L <= b ) ) by A5, YELLOW_0:30;
A7: xl is_>=_than Z1

proof

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:59;
assume b in Z1 ; :: thesis: b <= xl
then b1 <= "\/" Z1,L by A6, LATTICE3:def 9;
hence b <= xl by YELLOW_0:61; :: thesis: verum

end;

now

let b be Element of S; :: thesis: ( b is_>=_than Z1 implies xl <= b )
reconsider b1 = b as Element of L by YELLOW_0:59;
assume A8: b is_>=_than Z1 ; :: thesis: xl <= b
b1 is_>=_than Z1

proof

let c1 be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c1 in Z1 or c1 <= b1 )
assume A9: c1 in Z1 ; :: thesis: c1 <= b1
then reconsider c = c1 as Element of S ;
c <= b by A8, A9, LATTICE3:def 9;
hence c1 <= b1 by YELLOW_0:60; :: thesis: verum

end;

then "\/" Z1,L <= b1 by A5, YELLOW_0:30;
hence xl <= b by YELLOW_0:61; :: thesis: verum

end;

then "\/" Z1,S = "\/" Z1,L by A7, YELLOW_0:30;
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;

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

reconsider dS = Bottom S as Element of L by YELLOW_0:59;
reconsider dL = Bottom L as Element of S by A1;
S is lower-bounded by A4, A10, WAYBEL20:6;
then Bottom S <= dL by YELLOW_0:44;
then A11: dS <= Bottom L by YELLOW_0:60;
Bottom L <= dS by YELLOW_0:44;
then A12: dS = Bottom L by A11, YELLOW_0:def 3;
ex_sup_of Z,L by YELLOW_0:17;
then x in { ("\/" V,L) where V is finite Subset of X : ex_sup_of V,L } by A3, A10, A12;
hence x in finsups X by WAYBEL_0:def 27; :: thesis: verum

end;

end;

end;

hence x in finsups X ; :: thesis: verum