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

set ff = f_0 R;

set gg = UAp R;

for x being Subset of R holds (f_0 R) . x = (UAp R) . x

proof

hence
f_0 R = UAp R
; :: thesis: verum
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 }

.= (UAp R) . x by ROUGHS_2:def 11 ;

hence (f_0 R) . x = (UAp R) . x ; :: thesis: verum

end;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

(f_0 R) . x =
UAp x
by WW, Defff
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 }

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;proof

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 } )
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;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

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

.= (UAp R) . x by ROUGHS_2:def 11 ;

hence (f_0 R) . x = (UAp R) . x ; :: thesis: verum