let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for a, c being Element of
for b, d being Element of st [a,b] << [c,d] holds
( a << c & b << d )
let a, c be Element of ; :: thesis: for b, d being Element of st [a,b] << [c,d] holds
( a << c & b << d )
let b, d be Element of ; :: thesis: ( [a,b] << [c,d] implies ( a << c & b << d ) )
assume A1: for D being non empty directed Subset of st [c,d] <= sup D holds
ex e being Element of 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 d' = {d} as non empty directed Subset of by WAYBEL_0:5;
let D be non empty directed Subset of ; :: 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₁ )
A4: d <= sup d' by YELLOW_0:39;
( ex_sup_of D,S & ex_sup_of d',T ) by WAYBEL_0:75;
then sup [:D,d':] = [(sup D),(sup d')] by YELLOW_3:43;
then [c,d] <= sup [:D,d':] by A3, A4, YELLOW_3:11;
then consider e being Element of such that
A5: e in [:D,d':] 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:23;
hence a <= e `1 by A6, YELLOW_3:11; :: thesis: verum

end;

let D be non empty directed Subset of ; :: 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 A7: 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 by WAYBEL_0:5;
A8: c <= sup c' by YELLOW_0:39;
( ex_sup_of c',S & ex_sup_of D,T ) by WAYBEL_0:75;
then sup [:c',D:] = [(sup c'),(sup D)] by YELLOW_3:43;
then [c,d] <= sup [:c',D:] by A7, A8, YELLOW_3:11;
then consider e being Element of such that
A9: e in [:c',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:23;
hence b <= e `2 by A10, YELLOW_3:11; :: thesis: verum