let S, T be non empty reflexive antisymmetric up-complete RelStr ; 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; for b, d being Element of T st [a,b] << [c,d] holds
( a << c & b << d )
let b, d be Element of T; ( [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 )
; WAYBEL_3:def 1 ( 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
b << dproof
reconsider d9 =
{d} as non
empty directed Subset of
T by WAYBEL_0:5;
let D be non
empty directed Subset of
S;
WAYBEL_3:def 1 ( not c <= "\/" (D,S) or ex b1 being M3( the carrier of S) st
( b1 in D & a <= b1 ) )
assume A3:
c <= sup D
;
ex b1 being M3( the carrier of S) st
( b1 in D & a <= b1 )
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
;
( e `1 in D & a <= e `1 )
thus
e `1 in D
by A5, MCART_1:10;
a <= e `1
e = [(e `1),(e `2)]
by A2, MCART_1:21;
hence
a <= e `1
by A6, YELLOW_3:11;
verum
end;
let D be non empty directed Subset of T; WAYBEL_3:def 1 ( not d <= "\/" (D,T) or ex b1 being M3( the carrier of T) st
( b1 in D & b <= b1 ) )
assume A7:
d <= sup D
; ex b1 being M3( the carrier of T) st
( b1 in D & b <= b1 )
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
; ( e `2 in D & b <= e `2 )
thus
e `2 in D
by A9, MCART_1:10; b <= e `2
e = [(e `1),(e `2)]
by A2, MCART_1:21;
hence
b <= e `2
by A10, YELLOW_3:11; verum