theorem :: WAYBEL20:10

for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
[:f,g:] is filtered-infs-preserving