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 ) )
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
assume A2: 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 )
thus a << c :: thesis: b << d

proof

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