let R be non empty RelStr ; :: thesis: for f being Function of the carrier of R,(bool the carrier of R)

for u, w being Element of R

for x being Subset of R st f . u = f . w holds

( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

let f be Function of the carrier of R,(bool the carrier of R); :: thesis: for u, w being Element of R

for x being Subset of R st f . u = f . w holds

( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

let u, w be Element of R; :: thesis: for x being Subset of R st f . u = f . w holds

( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

let x be Subset of R; :: thesis: ( f . u = f . w implies ( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x ) )

assume AA: f . u = f . w ; :: thesis: ( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

A3: (Flip (ff_0 f)) . x = { w where w is Element of R : f . w c= x } by FlipFF;

thus ( u in (Flip (ff_0 f)) . x implies w in (Flip (ff_0 f)) . x ) :: thesis: ( w in (Flip (ff_0 f)) . x implies u in (Flip (ff_0 f)) . x )

then ex v being Element of R st

( w = v & f . v c= x ) by A3;

hence u in (Flip (ff_0 f)) . x by A3, AA; :: thesis: verum

for u, w being Element of R

for x being Subset of R st f . u = f . w holds

( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

let f be Function of the carrier of R,(bool the carrier of R); :: thesis: for u, w being Element of R

for x being Subset of R st f . u = f . w holds

( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

let u, w be Element of R; :: thesis: for x being Subset of R st f . u = f . w holds

( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

let x be Subset of R; :: thesis: ( f . u = f . w implies ( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x ) )

assume AA: f . u = f . w ; :: thesis: ( u in (Flip (ff_0 f)) . x iff w in (Flip (ff_0 f)) . x )

A3: (Flip (ff_0 f)) . x = { w where w is Element of R : f . w c= x } by FlipFF;

thus ( u in (Flip (ff_0 f)) . x implies w in (Flip (ff_0 f)) . x ) :: thesis: ( w in (Flip (ff_0 f)) . x implies u in (Flip (ff_0 f)) . x )

proof

assume
w in (Flip (ff_0 f)) . x
; :: thesis: u in (Flip (ff_0 f)) . x
assume
u in (Flip (ff_0 f)) . x
; :: thesis: w in (Flip (ff_0 f)) . x

then consider v being Element of R such that

A2: ( u = v & f . v c= x ) by A3;

thus w in (Flip (ff_0 f)) . x by A3, AA, A2; :: thesis: verum

end;then consider v being Element of R such that

A2: ( u = v & f . v c= x ) by A3;

thus w in (Flip (ff_0 f)) . x by A3, AA, A2; :: thesis: verum

then ex v being Element of R st

( w = v & f . v c= x ) by A3;

hence u in (Flip (ff_0 f)) . x by A3, AA; :: thesis: verum