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 --> ()) 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 --> ())) 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 --> ()) . c = RealPoset [.0,1.] & f . c <= g . c ) by A3;
hence f9 . c <<= g9 . c by Th3; :: thesis: verum
end;
hence (C,f) @ <<= (C,g) @ by ; :: 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 --> ())) 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 --> ()) . c = RealPoset [.0,1.] & ff . c <<= gg . c ) by ;
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