let R be non empty RelStr ; :: thesis: for u, w being Element of R
for x being Subset of R st () . u = () . w holds
( u in (Flip (f_1 R)) . x iff w in (Flip (f_1 R)) . x )

let u, w be Element of R; :: thesis: for x being Subset of R st () . u = () . w holds
( u in (Flip (f_1 R)) . x iff w in (Flip (f_1 R)) . x )

let x be Subset of R; :: thesis: ( () . u = () . w implies ( u in (Flip (f_1 R)) . x iff w in (Flip (f_1 R)) . x ) )
assume AA: (UncertaintyMap R) . u = () . w ; :: thesis: ( u in (Flip (f_1 R)) . x iff w in (Flip (f_1 R)) . x )
A3: (Flip (f_1 R)) . x = { w where w is Element of R : () . w c= x } by FlipF1;
thus ( u in (Flip (f_1 R)) . x implies w in (Flip (f_1 R)) . x ) :: thesis: ( w in (Flip (f_1 R)) . x implies u in (Flip (f_1 R)) . x )
proof
assume u in (Flip (f_1 R)) . x ; :: thesis: w in (Flip (f_1 R)) . x
then consider v being Element of R such that
A2: ( u = v & () . v c= x ) by A3;
thus w in (Flip (f_1 R)) . x by A3, AA, A2; :: thesis: verum
end;
assume w in (Flip (f_1 R)) . x ; :: thesis: u in (Flip (f_1 R)) . x
then ex v being Element of R st
( w = v & () . v c= x ) by A3;
hence u in (Flip (f_1 R)) . x by A3, AA; :: thesis: verum