let S be SubRelStr of L; :: thesis: ( S is infs-inheriting implies S is meet-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 meet-inheriting
let x, y be Element of L; :: according to YELLOW_0:def 16 :: thesis: ( x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L implies inf {x,y} in the carrier of S )
assume ( x in the carrier of S & y in the carrier of S ) ; :: thesis: ( not ex_inf_of {x,y},L or inf {x,y} in the carrier of S )
then {x,y} c= the carrier of S by ZFMISC_1:38;
hence ( not ex_inf_of {x,y},L or inf {x,y} in the carrier of S ) by A1; :: thesis: verum