let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for a, c being Element of S
for b, d being Element of T st [a,b] << [c,d] holds
( a << c & b << d )
let a, c be Element of S; :: thesis: for b, d being Element of T st [a,b] << [c,d] holds
( a << c & b << d )
let b, d be Element of T; :: thesis: ( [a,b] << [c,d] implies ( a << c & b << d ) )
assume A1: for D being non empty directed Subset of [:S,T:] st [c,d] <= sup D holds
ex e being Element of [:S,T:] st
( e in D & [a,b] <= e ) ; :: according to WAYBEL_3:def 1 :: thesis: ( a << c & b << d )
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
thus a << c :: thesis: b << d

proof

reconsider d9 = {d} as non empty directed Subset of T by WAYBEL_0:5;
let D be non empty directed Subset of S; :: according to WAYBEL_3:def 1 :: thesis: ( not c <= "\/" (D,S) or ex b₁ being M3( the carrier of S) st
( b₁ in D & a <= b₁ ) )
assume A3: c <= sup D ; :: thesis: ex b₁ being M3( the carrier of S) st
( b₁ in D & a <= b₁ )
A4: d <= sup d9 by YELLOW_0:39;
( ex_sup_of D,S & ex_sup_of d9,T ) by WAYBEL_0:75;
then sup [:D,d9:] = [(sup D),(sup d9)] by YELLOW_3:43;
then [c,d] <= sup [:D,d9:] by A3, A4, YELLOW_3:11;
then consider e being Element of [:S,T:] such that
A5: e in [:D,d9:] and
A6: [a,b] <= e by A1;
take e `1 ; :: thesis: ( e `1 in D & a <= e `1 )
thus e `1 in D by A5, MCART_1:10; :: thesis: a <= e `1
e = [(e `1),(e `2)] by A2, MCART_1:21;
hence a <= e `1 by A6, YELLOW_3:11; :: thesis: verum

end;

let D be non empty directed Subset of T; :: according to WAYBEL_3:def 1 :: thesis: ( not d <= "\/" (D,T) or ex b₁ being M3( the carrier of T) st
( b₁ in D & b <= b₁ ) )
assume A7: d <= sup D ; :: thesis: ex b₁ being M3( the carrier of T) st
( b₁ in D & b <= b₁ )
reconsider c9 = {c} as non empty directed Subset of S by WAYBEL_0:5;
A8: c <= sup c9 by YELLOW_0:39;
( ex_sup_of c9,S & ex_sup_of D,T ) by WAYBEL_0:75;
then sup [:c9,D:] = [(sup c9),(sup D)] by YELLOW_3:43;
then [c,d] <= sup [:c9,D:] by A7, A8, YELLOW_3:11;
then consider e being Element of [:S,T:] such that
A9: e in [:c9,D:] and
A10: [a,b] <= e by A1;
take e `2 ; :: thesis: ( e `2 in D & b <= e `2 )
thus e `2 in D by A9, MCART_1:10; :: thesis: b <= e `2
e = [(e `1),(e `2)] by A2, MCART_1:21;
hence b <= e `2 by A10, YELLOW_3:11; :: thesis: verum