theorem :: YELLOW_3:27

for S1, S2 being non empty reflexive RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds
( D1 is lower & D2 is lower )