let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of
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 ; :: 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 & 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
A2: ( g in X & y = g . i ) by CARD_3:def 6;
reconsider f = f, g = g as Element of (product J) by A1, A2;
consider h being Element of (product J) such that
A3: ( h in X & f <= h & g <= h ) by A1, A2, 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 A3, CARD_3:def 6; :: thesis: ( x <= h . i & y <= h . i )
thus ( x <= h . i & y <= h . i ) by A1, A2, A3, WAYBEL_3:28; :: thesis: verum