theorem Th27: :: WAYBEL_0:27

for L being RelStr
for X, Y being Subset of L st X is lower & Y is lower holds
( X /\ Y is lower & X \/ Y is lower )