let T be upper-bounded Semilattice; :: thesis:
let S be non empty full meet-inheriting SubRelStr of T; :: thesis:
assume that
A1: Top T in the carrier of S and
A2: S is filtered-infs-inheriting ; :: thesis:
let A be Subset of S; :: according to YELLOW_0:def 18 :: thesis:
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then reconsider C = A as Subset of T by XBOOLE_1:1;
set F = fininfs C;
assume A3: ex_inf_of A,T ; :: thesis:
then A4: inf (fininfs C) = inf C by WAYBEL_0:60;
fininfs C c= the carrier of S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in fininfs C ; :: thesis:
then consider Y being finite Subset of C such that
A5: x = "/\" (Y,T) and
ex_inf_of Y,T ;
reconsider Y = Y as finite Subset of T by XBOOLE_1:1;
reconsider Z = Y as finite Subset of S by XBOOLE_1:1;
assume A6: not x in the carrier of S ; :: thesis:
then Z <> {} by A1, A5;
hence contradiction by A5, A6, Th14; :: thesis:

end;

then reconsider G = fininfs C as non empty Subset of S ;
reconsider G = G as non empty filtered Subset of S by WAYBEL10:23;

A7: now :: thesis:

let Y be finite Subset of C; :: thesis:
Y c= the carrier of T by XBOOLE_1:1;
hence ( Y <> {} implies ex_inf_of Y,T ) by YELLOW_0:55; :: thesis:

end;

A8: now :: thesis:

let x be Element of T; :: thesis:
assume x in fininfs C ; :: thesis:
then ex Y being finite Subset of C st
( x = "/\" (Y,T) & ex_inf_of Y,T ) ;
hence ex Y being finite Subset of C st
( ex_inf_of Y,T & x = "/\" (Y,T) ) ; :: thesis:

end;

now :: thesis:

let Y be finite Subset of C; :: thesis:
reconsider Z = Y as finite Subset of T by XBOOLE_1:1;
assume Y <> {} ; :: thesis:
then ex_inf_of Z,T by YELLOW_0:55;
hence "/\" (Y,T) in fininfs C ; :: thesis:

end;

then ex_inf_of G,T by A3, A7, A8, WAYBEL_0:58;
hence "/\" (A,T) in the carrier of S by A2, A4; :: thesis: