:: deftheorem defines infs-inheriting YELLOW_0:def 18 :
for L being non empty RelStr
for S being SubRelStr of L holds
( S is infs-inheriting iff for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in the carrier of S );