let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of
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 ; :: 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 9 :: thesis: ( not x in pi X,i or x <= f . i )
assume x in pi X,i ; :: thesis: x <= f . i
then consider g being Function such that
A2: ( g in X & x = g . i ) by CARD_3:def 6;
reconsider g = g as Element of (product J) by A2;
g <= f by A1, A2, LATTICE3:def 9;
hence x <= f . i by A2, WAYBEL_3:28; :: thesis: verum

end;

end;

assume A3: 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 9 :: thesis: ( not g in X or g <= f )
assume A4: g in X ; :: thesis: g <= f

now

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

end;

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