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) @ )

( ( 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

( (C,f) @ <<= (C,g) @ implies for c being Element of C holds f . c <= g . c )
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

end;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

hence
(C,f) @ <<= (C,g) @
by A1, WAYBEL_3:28; :: thesis: verum
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;

hence f9 . c <<= g9 . c by Th3; :: thesis: verum

end;set f1 = f . c;

set g1 = g . c;

( (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] & f . c <= g . c ) by A3;

hence f9 . c <<= g9 . c by Th3; :: thesis: verum

proof

hence
( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ )
by A2; :: thesis: verum
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;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