theorem :: WAYBEL23:34

for L being non empty RelStr
for S1, S2 being meet-closed Subset of L holds S1 /\ S2 is meet-closed