let C be non empty set ; 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; ( ( 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
;
(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;
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)
@
;
for c being Element of C holds f . c <= g . c
let c be
Element of
C;
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;
verum
end;
hence
( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ )
by A2; verum