let T be sup-Semilattice; :: thesis: for S being non empty full SubRelStr of T holds
( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S )
let S be non empty full SubRelStr of T; :: thesis: ( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S )

hereby :: thesis: ( ( for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ) implies S is join-inheriting )

assume A1: S is join-inheriting ; :: thesis: for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S
let X be non empty finite Subset of S; :: thesis: "\/" (X,T) in the carrier of S
A2: X is finite ;
defpred S₁[ set ] means ( $1 <> {} implies "\/" ($1,T) in the carrier of S );
A3: S₁[ {} ] ;

A4: now :: thesis: for y, x being set st y in X & x c= X & S₁[x] holds
S₁[x \/ {y}]

let y, x be set ; :: thesis: ( y in X & x c= X & S₁[x] implies S₁[x \/ {y}] )
assume that
A5: y in X and
A6: x c= X and
A7: S₁[x] ; :: thesis: S₁[x \/ {y}]
reconsider y9 = y as Element of S by A5;
reconsider z = y9 as Element of T by YELLOW_0:58;
thus S₁[x \/ {y}] :: thesis: verum

proof

assume x \/ {y} <> {} ; :: thesis: "\/" ((x \/ {y}),T) in the carrier of S
A8: x c= the carrier of S by A6, XBOOLE_1:1;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then reconsider x9 = x as finite Subset of T by A6, A8, XBOOLE_1:1;
A9: ex_sup_of {z},T by YELLOW_0:38;
A10: sup {z} = y9 by YELLOW_0:39;

now :: thesis: ( x9 <> {} implies sup (x9 \/ {z}) in the carrier of S )

assume A11: x9 <> {} ; :: thesis: sup (x9 \/ {z}) in the carrier of S
then ex_sup_of x9,T by YELLOW_0:54;
then A12: sup (x9 \/ {z}) = (sup x9) "\/" z by A9, A10, YELLOW_2:3;
ex_sup_of {(sup x9),z},T by YELLOW_0:20;
then sup {(sup x9),z} in the carrier of S by A1, A7, A11;
hence sup (x9 \/ {z}) in the carrier of S by A12, YELLOW_0:41; :: thesis: verum

end;

hence "\/" ((x \/ {y}),T) in the carrier of S by A10; :: thesis: verum

end;

end;

S₁[X] from FINSET_1:sch 2(A2, A3, A4);
hence "\/" (X,T) in the carrier of S ; :: thesis: verum

end;

assume A13: for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S ; :: thesis: S is join-inheriting
let x, y be Element of T; :: according to YELLOW_0:def 17 :: thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S )
assume that
A14: x in the carrier of S and
A15: y in the carrier of S ; :: thesis: ( not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S )
{x,y} c= the carrier of S by A14, A15, ZFMISC_1:32;
hence ( not ex_sup_of {x,y},T or "\/" ({x,y},T) in the carrier of S ) by A13; :: thesis: verum