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 (ff_0 f) . x iff w in (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 (ff_0 f) . x iff w in (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 (ff_0 f) . x iff w in (ff_0 f) . x )
let x be Subset of R; :: thesis: ( f . u = f . w implies ( u in (ff_0 f) . x iff w in (ff_0 f) . x ) )
assume AA: f . u = f . w ; :: thesis: ( u in (ff_0 f) . x iff w in (ff_0 f) . x )
A3: (ff_0 f) . x = { w where w is Element of R : f . w meets x } by Defff;
thus ( u in (ff_0 f) . x implies w in (ff_0 f) . x ) :: thesis: ( w in (ff_0 f) . x implies u in (ff_0 f) . x )

proof

assume A1: u in (ff_0 f) . x ; :: thesis: w in (ff_0 f) . x
consider v being Element of R such that
A2: ( u = v & f . v meets x ) by A1, A3;
thus w in (ff_0 f) . x by A3, AA, A2; :: thesis: verum

end;

assume w in (ff_0 f) . x ; :: thesis: u in (ff_0 f) . x
then consider v being Element of R such that
A2: ( w = v & f . v meets x ) by A3;
thus u in (ff_0 f) . x by A3, AA, A2; :: thesis: verum