for a, b being Subset of A holds f . (a /\ b) = (f . a) /\ (f . b)
by ROUGHS_4:def 10;

then for a, b being Subset of A holds (Flip f) . (a \/ b) = ((Flip f) . a) \/ ((Flip f) . b) by ROUGHS_2:22;

hence Flip f is \/-preserving by ROUGHS_4:def 9; :: thesis: verum

then for a, b being Subset of A holds (Flip f) . (a \/ b) = ((Flip f) . a) \/ ((Flip f) . b) by ROUGHS_2:22;

hence Flip f is \/-preserving by ROUGHS_4:def 9; :: thesis: verum