theorem Th29: :: WAYBEL_0:29

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