let S, T be non empty reflexive RelStr ; ( [:S,T:] is /\-complete implies ( S is /\-complete & T is /\-complete ) )
assume A1:
for X being non empty Subset of [:S,T:] ex x being Element of [:S,T:] st
( x is_<=_than X & ( for y being Element of [:S,T:] st y is_<=_than X holds
x >= y ) )
; WAYBEL_0:def 40 ( S is /\-complete & T is /\-complete )
A2:
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
thus
S is /\-complete
T is /\-complete proof
set t = the
Element of
T;
let X be non
empty Subset of
S;
WAYBEL_0:def 40 ex b1 being M3( the carrier of S) st
( b1 is_<=_than X & ( for b2 being M3( the carrier of S) holds
( not b2 is_<=_than X or b2 <= b1 ) ) )
consider x being
Element of
[:S,T:] such that A3:
x is_<=_than [:X,{ the Element of T}:]
and A4:
for
y being
Element of
[:S,T:] st
y is_<=_than [:X,{ the Element of T}:] holds
x >= y
by A1;
take
x `1
;
( x `1 is_<=_than X & ( for b1 being M3( the carrier of S) holds
( not b1 is_<=_than X or b1 <= x `1 ) ) )
A5:
x = [(x `1),(x `2)]
by A2, MCART_1:21;
hence
x `1 is_<=_than X
by A3, YELLOW_3:32;
for b1 being M3( the carrier of S) holds
( not b1 is_<=_than X or b1 <= x `1 )
the
Element of
T <= the
Element of
T
;
then A6:
the
Element of
T is_<=_than { the Element of T}
by YELLOW_0:7;
let y be
Element of
S;
( not y is_<=_than X or y <= x `1 )
assume
y is_<=_than X
;
y <= x `1
then
x >= [y, the Element of T]
by A4, A6, YELLOW_3:33;
hence
y <= x `1
by A5, YELLOW_3:11;
verum
end;
set s = the Element of S;
let X be non empty Subset of T; WAYBEL_0:def 40 ex b1 being M3( the carrier of T) st
( b1 is_<=_than X & ( for b2 being M3( the carrier of T) holds
( not b2 is_<=_than X or b2 <= b1 ) ) )
consider x being Element of [:S,T:] such that
A7:
x is_<=_than [:{ the Element of S},X:]
and
A8:
for y being Element of [:S,T:] st y is_<=_than [:{ the Element of S},X:] holds
x >= y
by A1;
take
x `2
; ( x `2 is_<=_than X & ( for b1 being M3( the carrier of T) holds
( not b1 is_<=_than X or b1 <= x `2 ) ) )
A9:
x = [(x `1),(x `2)]
by A2, MCART_1:21;
hence
x `2 is_<=_than X
by A7, YELLOW_3:32; for b1 being M3( the carrier of T) holds
( not b1 is_<=_than X or b1 <= x `2 )
the Element of S <= the Element of S
;
then A10:
the Element of S is_<=_than { the Element of S}
by YELLOW_0:7;
let y be Element of T; ( not y is_<=_than X or y <= x `2 )
assume
y is_<=_than X
; y <= x `2
then
x >= [ the Element of S,y]
by A8, A10, YELLOW_3:33;
hence
y <= x `2
by A9, YELLOW_3:11; verum