let R be non empty RelStr ; :: thesis: for x, y being Subset of R holds ((Flip (f_0 R)) . x) /\ ((Flip (f_0 R)) . y) = (Flip (f_0 R)) . (x /\ y)
let x, y be Subset of R; :: thesis: ((Flip (f_0 R)) . x) /\ ((Flip (f_0 R)) . y) = (Flip (f_0 R)) . (x /\ y)
set f = tau R;
thus ((Flip (f_0 R)) . x) /\ ((Flip (f_0 R)) . y) = (Flip (f_0 R)) . (x /\ y) by Propm; :: thesis: verum