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 by A3, Th3;
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, 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