let R be non empty RelStr ; :: thesis: f_0 R = UAp R
set ff = f_0 R;
set gg = UAp R;
for x being Subset of R holds (f_0 R) . x = (UAp R) . x

proof

let x be Subset of R; :: thesis: (f_0 R) . x = (UAp R) . x
WW: { u where u is Element of R : (tau R) . u meets x } = { w where w is Element of R : Class ( the InternalRel of R,w) meets x }

proof

thus { u where u is Element of R : (tau R) . u meets x } c= { w where w is Element of R : Class ( the InternalRel of R,w) meets x } :: according to XBOOLE_0:def 10 :: thesis: { w where w is Element of R : Class ( the InternalRel of R,w) meets x } c= { u where u is Element of R : (tau R) . u meets x }

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { u where u is Element of R : (tau R) . u meets x } or t in { w where w is Element of R : Class ( the InternalRel of R,w) meets x } )
assume t in { u where u is Element of R : (tau R) . u meets x } ; :: thesis: t in { w where w is Element of R : Class ( the InternalRel of R,w) meets x }
then consider u being Element of R such that
W1: ( u = t & (tau R) . u meets x ) ;
consider tt being object such that
W2: ( tt in (tau R) . u & tt in x ) by XBOOLE_0:3, W1;
W4: (tau R) . u = Im ( the InternalRel of R,u) by DefTau;
reconsider ttt = tt as Element of R by W2;
thus t in { w where w is Element of R : Class ( the InternalRel of R,w) meets x } by W1, W4; :: thesis: verum

end;

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { w where w is Element of R : Class ( the InternalRel of R,w) meets x } or t in { u where u is Element of R : (tau R) . u meets x } )
assume t in { w where w is Element of R : Class ( the InternalRel of R,w) meets x } ; :: thesis: t in { u where u is Element of R : (tau R) . u meets x }
then consider tt being Element of R such that
H1: ( tt = t & Class ( the InternalRel of R,tt) meets x ) ;
consider wx being object such that
H2: ( wx in Class ( the InternalRel of R,tt) & wx in x ) by H1, XBOOLE_0:3;
reconsider wxx = wx as Element of R by H2;
(tau R) . tt = Im ( the InternalRel of R,tt) by DefTau;
hence t in { u where u is Element of R : (tau R) . u meets x } by H1; :: thesis: verum

end;

(f_0 R) . x = UAp x by WW, Defff
.= (UAp R) . x by ROUGHS_2:def 11 ;
hence (f_0 R) . x = (UAp R) . x ; :: thesis: verum

end;

hence f_0 R = UAp R ; :: thesis: verum