let T be upper-bounded Semilattice; :: thesis: for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & S is filtered-infs-inheriting holds
S is infs-inheriting
let S be non empty full meet-inheriting SubRelStr of T; :: thesis: ( Top T in the carrier of S & S is filtered-infs-inheriting implies S is infs-inheriting )
assume that
A1: Top T in the carrier of S and
A2: S is filtered-infs-inheriting ; :: thesis: S is infs-inheriting
let A be Subset of S; :: according to YELLOW_0:def 18 :: thesis: ( not ex_inf_of A,T or "/\" (A,T) in the carrier of S )
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: "/\" (A,T) in the carrier of S
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: ( not x in fininfs C or x in the carrier of S )
assume x in fininfs C ; :: thesis: x in the carrier of S
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: contradiction
then Z <> {} by A1, A5;
hence contradiction by A5, A6, Th14; :: thesis: verum

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: for Y being finite Subset of C st Y <> {} holds
ex_inf_of Y,T

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

end;

A8: now :: thesis: for x being Element of T st x in fininfs C holds
ex Y being finite Subset of C st
( ex_inf_of Y,T & x = "/\" (Y,T) )

let x be Element of T; :: thesis: ( x in fininfs C implies ex Y being finite Subset of C st
( ex_inf_of Y,T & x = "/\" (Y,T) ) )
assume x in fininfs C ; :: thesis: ex Y being finite Subset of C st
( ex_inf_of Y,T & x = "/\" (Y,T) )
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: verum

end;

now :: thesis: for Y being finite Subset of C st Y <> {} holds
"/\" (Y,T) in fininfs C

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

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: verum