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
consider t being
Element of
T;
let X be non
empty Subset of
S;
WAYBEL_0:def 40 ex b1 being M2(the carrier of S) st
( b1 is_<=_than X & ( for b2 being M2(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,{t}:]
and A4:
for
y being
Element of
[:S,T:] st
y is_<=_than [:X,{t}:] holds
x >= y
by A1;
take
x `1
;
( x `1 is_<=_than X & ( for b1 being M2(the carrier of S) holds
( not b1 is_<=_than X or b1 <= x `1 ) ) )
A5:
x = [(x `1 ),(x `2 )]
by A2, MCART_1:23;
hence
x `1 is_<=_than X
by A3, YELLOW_3:32;
for b1 being M2(the carrier of S) holds
( not b1 is_<=_than X or b1 <= x `1 )
t <= t
;
then A6:
t is_<=_than {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,t]
by A4, A6, YELLOW_3:33;
hence
y <= x `1
by A5, YELLOW_3:11;
verum
end;
consider s being Element of S;
let X be non empty Subset of T; WAYBEL_0:def 40 ex b1 being M2(the carrier of T) st
( b1 is_<=_than X & ( for b2 being M2(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 [:{s},X:]
and
A8:
for y being Element of [:S,T:] st y is_<=_than [:{s},X:] holds
x >= y
by A1;
take
x `2
; ( x `2 is_<=_than X & ( for b1 being M2(the carrier of T) holds
( not b1 is_<=_than X or b1 <= x `2 ) ) )
A9:
x = [(x `1 ),(x `2 )]
by A2, MCART_1:23;
hence
x `2 is_<=_than X
by A7, YELLOW_3:32; for b1 being M2(the carrier of T) holds
( not b1 is_<=_than X or b1 <= x `2 )
s <= s
;
then A10:
s is_<=_than {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 >= [s,y]
by A8, A10, YELLOW_3:33;
hence
y <= x `2
by A9, YELLOW_3:11; verum