theorem :: YELLOW_3:24

for S1, S2 being non empty reflexive RelStr
for D being non empty filtered Subset of [:S1,S2:] holds
( proj1 D is filtered & proj2 D is filtered )