:: deftheorem Def3 defines filtered-infs-inheriting WAYBEL_0:def 3 :
for L being non empty RelStr
for S being SubRelStr of L holds
( S is filtered-infs-inheriting iff for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
"/\" (X,L) in the carrier of S );