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