let S be SubRelStr of L; :: thesis: ( S is infs-inheriting implies S is filtered-infs-inheriting )
assume A1: for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in the carrier of S ; :: according to YELLOW_0:def 18 :: thesis: S is filtered-infs-inheriting
let X be filtered Subset of S; :: according to WAYBEL_0:def 3 :: thesis: ( X <> {} & ex_inf_of X,L implies "/\" (X,L) in the carrier of S )
thus ( X <> {} & ex_inf_of X,L implies "/\" (X,L) in the carrier of S ) by A1; :: thesis: verum