let S be SubRelStr of L; ( 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
; YELLOW_0:def 18 S is meet-inheriting
let x, y be Element of L; YELLOW_0:def 16 ( 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 )
; ( 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:32;
hence
( not ex_inf_of {x,y},L or inf {x,y} in the carrier of S )
by A1; verum