let R be non empty RelStr ; :: thesis: for u, w being Element of R

for x being Subset of R st (tau R) . u = (tau R) . w holds

( u in (f_0 R) . x iff w in (f_0 R) . x )

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

( u in (f_0 R) . x iff w in (f_0 R) . x )

let x be Subset of R; :: thesis: ( (tau R) . u = (tau R) . w implies ( u in (f_0 R) . x iff w in (f_0 R) . x ) )

assume AA: (tau R) . u = (tau R) . w ; :: thesis: ( u in (f_0 R) . x iff w in (f_0 R) . x )

A3: (f_0 R) . x = { w where w is Element of R : (tau R) . w meets x } by Defff;

thus ( u in (f_0 R) . x implies w in (f_0 R) . x ) :: thesis: ( w in (f_0 R) . x implies u in (f_0 R) . x )

then A2: ex v being Element of R st

( w = v & (tau R) . v meets x ) by A3;

thus u in (f_0 R) . x by A3, AA, A2; :: thesis: verum

for x being Subset of R st (tau R) . u = (tau R) . w holds

( u in (f_0 R) . x iff w in (f_0 R) . x )

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

( u in (f_0 R) . x iff w in (f_0 R) . x )

let x be Subset of R; :: thesis: ( (tau R) . u = (tau R) . w implies ( u in (f_0 R) . x iff w in (f_0 R) . x ) )

assume AA: (tau R) . u = (tau R) . w ; :: thesis: ( u in (f_0 R) . x iff w in (f_0 R) . x )

A3: (f_0 R) . x = { w where w is Element of R : (tau R) . w meets x } by Defff;

thus ( u in (f_0 R) . x implies w in (f_0 R) . x ) :: thesis: ( w in (f_0 R) . x implies u in (f_0 R) . x )

proof

assume
w in (f_0 R) . x
; :: thesis: u in (f_0 R) . x
assume A1:
u in (f_0 R) . x
; :: thesis: w in (f_0 R) . x

then consider v being Element of R such that

A2: ( u = v & (tau R) . v meets x ) by A3;

thus w in (f_0 R) . x by A3, AA, A2; :: thesis: verum

end;then consider v being Element of R such that

A2: ( u = v & (tau R) . v meets x ) by A3;

thus w in (f_0 R) . x by A3, AA, A2; :: thesis: verum

then A2: ex v being Element of R st

( w = v & (tau R) . v meets x ) by A3;

thus u in (f_0 R) . x by A3, AA, A2; :: thesis: verum