let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
for X being directed Subset of (product J)
for i being Element of I holds pi (X,i) is directed
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis: for X being directed Subset of (product J)
for i being Element of I holds pi (X,i) is directed
let X be directed Subset of (product J); :: thesis: for i being Element of I holds pi (X,i) is directed
let i be Element of I; :: thesis: pi (X,i) is directed
let x, y be Element of (J . i); :: according to WAYBEL_0:def 1 :: thesis: ( not x in pi (X,i) or not y in pi (X,i) or ex b₁ being Element of the carrier of (J . i) st
( b₁ in pi (X,i) & x <= b₁ & y <= b₁ ) )
assume x in pi (X,i) ; :: thesis: ( not y in pi (X,i) or ex b₁ being Element of the carrier of (J . i) st
( b₁ in pi (X,i) & x <= b₁ & y <= b₁ ) )
then consider f being Function such that
A1: f in X and
A2: x = f . i by CARD_3:def 6;
assume y in pi (X,i) ; :: thesis: ex b₁ being Element of the carrier of (J . i) st
( b₁ in pi (X,i) & x <= b₁ & y <= b₁ )
then consider g being Function such that
A3: g in X and
A4: y = g . i by CARD_3:def 6;
reconsider f = f, g = g as Element of (product J) by A1, A3;
consider h being Element of (product J) such that
A5: h in X and
A6: f <= h and
A7: g <= h by A1, A3, WAYBEL_0:def 1;
take h . i ; :: thesis: ( h . i in pi (X,i) & x <= h . i & y <= h . i )
thus h . i in pi (X,i) by A5, CARD_3:def 6; :: thesis: ( x <= h . i & y <= h . i )
thus ( x <= h . i & y <= h . i ) by A2, A4, A6, A7, WAYBEL_3:28; :: thesis: verum