let T be Semilattice; :: thesis: for S being non empty full SubRelStr of T holds
( S is meet-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 meet-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 meet-inheriting )

assume A1: S is meet-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}]
thus S₁[x \/ {y}] :: thesis: verum

proof

assume x \/ {y} <> {} ; :: thesis: "/\" ((x \/ {y}),T) in the carrier of S
reconsider y9 = y as Element of S by A5;
reconsider z = y9 as Element of T by YELLOW_0:58;
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_inf_of {z},T by YELLOW_0:38;
A10: inf {z} = y9 by YELLOW_0:39;

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

assume A11: x9 <> {} ; :: thesis: inf (x9 \/ {z}) in the carrier of S
then ex_inf_of x9,T by YELLOW_0:55;
then A12: inf (x9 \/ {z}) = (inf x9) "/\" z by A9, A10, YELLOW_2:4;
ex_inf_of {(inf x9),z},T by YELLOW_0:21;
then inf {(inf x9),z} in the carrier of S by A1, A7, A11;
hence inf (x9 \/ {z}) in the carrier of S by A12, YELLOW_0:40; :: 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 meet-inheriting
let x, y be Element of T; :: according to YELLOW_0:def 16 :: thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_inf_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_inf_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_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S ) by A13; :: thesis: verum