let N be Semilattice; :: thesis: for A being Subset of N st subrelstr A is meet-inheriting holds
A is filtered
let A be Subset of N; :: thesis: ( subrelstr A is meet-inheriting implies A is filtered )
assume A1: subrelstr A is meet-inheriting ; :: thesis: A is filtered
let x, y be Element of N; :: according to WAYBEL_0:def 2 :: thesis: ( not x in A or not y in A or ex b₁ being Element of the carrier of N st
( b₁ in A & b₁ <= x & b₁ <= y ) )
assume A2: ( x in A & y in A ) ; :: thesis: ex b₁ being Element of the carrier of N st
( b₁ in A & b₁ <= x & b₁ <= y )
take x "/\" y ; :: thesis: ( x "/\" y in A & x "/\" y <= x & x "/\" y <= y )
A3: the carrier of (subrelstr A) = A by YELLOW_0:def 15;
ex_inf_of {x,y},N by YELLOW_0:21;
then inf {x,y} in the carrier of (subrelstr A) by A1, A2, A3;
hence x "/\" y in A by A3, YELLOW_0:40; :: thesis: ( x "/\" y <= x & x "/\" y <= y )
thus ( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23; :: thesis: verum