let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of I
for f being Element of (product J)
for X being Subset of (product J) holds
( f is_<=_than X iff for i being Element of I holds f . i is_<=_than pi (X,i) )
let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: for f being Element of (product J)
for X being Subset of (product J) holds
( f is_<=_than X iff for i being Element of I holds f . i is_<=_than pi (X,i) )
let f be Element of (product J); :: thesis: for X being Subset of (product J) holds
( f is_<=_than X iff for i being Element of I holds f . i is_<=_than pi (X,i) )
let X be Subset of (product J); :: thesis: ( f is_<=_than X iff for i being Element of I holds f . i is_<=_than pi (X,i) )

hereby :: thesis: ( ( for i being Element of I holds f . i is_<=_than pi (X,i) ) implies f is_<=_than X )

assume A1: f is_<=_than X ; :: thesis: for i being Element of I holds f . i is_<=_than pi (X,i)
let i be Element of I; :: thesis: f . i is_<=_than pi (X,i)
thus f . i is_<=_than pi (X,i) :: thesis: verum

proof

let x be Element of (J . i); :: according to LATTICE3:def 8 :: thesis: ( not x in pi (X,i) or f . i <= x )
assume x in pi (X,i) ; :: thesis: f . i <= x
then consider g being Function such that
A2: g in X and
A3: x = g . i by CARD_3:def 6;
reconsider g = g as Element of (product J) by A2;
g >= f by A1, A2;
hence f . i <= x by A3, WAYBEL_3:28; :: thesis: verum

end;

end;

assume A4: for i being Element of I holds f . i is_<=_than pi (X,i) ; :: thesis: f is_<=_than X
let g be Element of (product J); :: according to LATTICE3:def 8 :: thesis: ( not g in X or f <= g )
assume A5: g in X ; :: thesis: f <= g

now :: thesis: for i being Element of I holds g . i >= f . i

let i be Element of I; :: thesis: g . i >= f . i
A6: f . i is_<=_than pi (X,i) by A4;
g . i in pi (X,i) by A5, CARD_3:def 6;
hence g . i >= f . i by A6; :: thesis: verum

end;

hence f <= g by WAYBEL_3:28; :: thesis: verum