let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds
( ( for c being Element of C holds f . c <= g . c ) iff C,f @ <<= C,g @ )
let f, g be Membership_Func of C; :: thesis: ( ( for c being Element of C holds f . c <= g . c ) iff C,f @ <<= C,g @ )
A1: (RealPoset [.0 ,1.]) |^ C = product (C --> (RealPoset [.0 ,1.])) by YELLOW_1:def 5;
A2: ( ( for c being Element of C holds f . c <= g . c ) implies C,f @ <<= C,g @ )

proof

set f9 = C,f @ ;
set g9 = C,g @ ;
reconsider f9 = C,f @ , g9 = C,g @ as Element of (product (C --> (RealPoset [.0 ,1.]))) by YELLOW_1:def 5;
assume A3: for c being Element of C holds f . c <= g . c ; :: thesis: C,f @ <<= C,g @
for c being Element of C holds f9 . c <<= g9 . c

proof

let c be Element of C; :: thesis: f9 . c <<= g9 . c
set f1 = f . c;
set g1 = g . c;
( (C --> (RealPoset [.0 ,1.])) . c = RealPoset [.0 ,1.] & f . c <= g . c ) by A3, FUNCOP_1:13;
hence f9 . c <<= g9 . c by Th3; :: thesis: verum

end;

hence C,f @ <<= C,g @ by A1, WAYBEL_3:28; :: thesis: verum

end;

( C,f @ <<= C,g @ implies for c being Element of C holds f . c <= g . c )

proof

reconsider ff = C,f @ , gg = C,g @ as Element of (product (C --> (RealPoset [.0 ,1.]))) by YELLOW_1:def 5;
assume A4: C,f @ <<= C,g @ ; :: thesis: for c being Element of C holds f . c <= g . c
let c be Element of C; :: thesis: f . c <= g . c
( (C --> (RealPoset [.0 ,1.])) . c = RealPoset [.0 ,1.] & ff . c <<= gg . c ) by A1, A4, FUNCOP_1:13, WAYBEL_3:28;
hence f . c <= g . c by Th3; :: thesis: verum

end;

hence ( ( for c being Element of C holds f . c <= g . c ) iff C,f @ <<= C,g @ ) by A2; :: thesis: verum