let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds R (#) (Imf (X,X)) = R
let R be RMembership_Func of X,X; :: thesis: R (#) (Imf (X,X)) = R
A1: for x, y being object st [x,y] in dom (R (#) (Imf (X,X))) holds
(R (#) (Imf (X,X))) . (x,y) = R . (x,y)

proof

let x, y be object ; :: thesis: ( [x,y] in dom (R (#) (Imf (X,X))) implies (R (#) (Imf (X,X))) . (x,y) = R . (x,y) )
assume [x,y] in dom (R (#) (Imf (X,X))) ; :: thesis: (R (#) (Imf (X,X))) . (x,y) = R . (x,y)
then reconsider x = x, y = y as Element of X by ZFMISC_1:87;
set S = { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ;
for c being Element of (RealPoset [.0,1.]) st c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } holds
c <<= R . [x,y]

proof

let c be Element of (RealPoset [.0,1.]); :: thesis: ( c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } implies c <<= R . [x,y] )
assume c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ; :: thesis: c <<= R . [x,y]
then consider z being Element of X such that
A2: c = (R . (x,z)) "/\" ((Imf (X,X)) . (z,y)) ;

per cases ( y = z or not y = z ) ;

suppose A3: y = z ; :: thesis: c <<= R . [x,y]

A4: R . (x,z) <= 1 by FUZZY_4:4;
c = min ((R . [x,z]),1) by A2, A3, FUZZY_4:25
.= R . [x,y] by A3, A4, XXREAL_0:def 9 ;
hence c <<= R . [x,y] by LFUZZY_0:3; :: thesis: verum

end;

suppose A5: not y = z ; :: thesis: c <<= R . [x,y]

A6: 0 <= R . (x,z) by FUZZY_4:4;
c = min ((R . [x,z]),0) by A2, A5, FUZZY_4:25
.= 0 by A6, XXREAL_0:def 9 ;
then c <= R . (x,y) by FUZZY_4:4;
hence c <<= R . [x,y] by LFUZZY_0:3; :: thesis: verum

end;

end;

end;

then A7: ( (R (#) (Imf (X,X))) . (x,y) = "\/" ( { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ,(RealPoset [.0,1.])) & R . (x,y) is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ) by LATTICE3:def 9, LFUZZY_0:22;
for b being Element of (RealPoset [.0,1.]) st b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } holds
R . (x,y) <<= b

proof

let b be Element of (RealPoset [.0,1.]); :: thesis: ( b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } implies R . (x,y) <<= b )
A8: R . (x,y) <= 1 by FUZZY_4:4;
(R . [x,y]) "/\" ((Imf (X,X)) . (y,y)) = min ((R . [x,y]),1) by FUZZY_4:25
.= R . [x,y] by A8, XXREAL_0:def 9 ;
then A9: R . (x,y) in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ;
assume b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ; :: thesis: R . (x,y) <<= b
hence R . (x,y) <<= b by A9, LATTICE3:def 9; :: thesis: verum

end;

hence (R (#) (Imf (X,X))) . (x,y) = R . (x,y) by A7, YELLOW_0:32; :: thesis: verum

end;

dom (R (#) (Imf (X,X))) = [:X,X:] by FUNCT_2:def 1
.= dom R by FUNCT_2:def 1 ;
hence R (#) (Imf (X,X)) = R by A1, BINOP_1:20; :: thesis: verum