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 set st [x,y] in dom (R (#) (Imf X,X)) holds
(R (#) (Imf X,X)) . x,y = R . x,y

proof

let x, y be set ; :: 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:106;
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:32; :: thesis: verum