let T be Semilattice; :: thesis:
let S be non empty full SubRelStr of T; :: thesis:

hereby :: thesis:

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

A4: now :: thesis:

let y, x be set ; :: thesis:
assume that
A5: y in X and
A6: x c= X and
A7: S₁[x] ; :: thesis:
thus S₁[x \/ {y}] :: thesis:

assume x \/ {y} <> {} ; :: thesis:
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;

assume A11: x9 <> {} ; :: thesis:
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:

end;

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

end;

end;

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

end;

assume A13: for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ; :: thesis:
let x, y be Element of T; :: according to YELLOW_0:def 16 :: thesis:
assume that
A14: x in the carrier of S and
A15: y in the carrier of S ; :: thesis:
{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: