let S, T be non empty reflexive RelStr ; :: thesis: ( [: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 ) )
; :: according to WAYBEL_0:def 40 :: thesis: ( 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
:: thesis: T is /\-completeproof
let X be non
empty Subset of
S;
:: according to WAYBEL_0:def 40 :: thesis: 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 t being
Element of
T;
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
;
:: thesis: ( 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;
:: thesis: for b1 being M2(the carrier of S) holds
( not b1 is_<=_than X or b1 <= x `1 )
let y be
Element of
S;
:: thesis: ( not y is_<=_than X or y <= x `1 )
assume A6:
y is_<=_than X
;
:: thesis: y <= x `1
t <= t
;
then
t is_<=_than {t}
by YELLOW_0:7;
then
x >= [y,t]
by A4, A6, YELLOW_3:33;
hence
x `1 >= y
by A5, YELLOW_3:11;
:: thesis: verum
end;
let X be non empty Subset of T; :: according to WAYBEL_0:def 40 :: thesis: 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 s being Element of S;
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
; :: thesis: ( 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; :: thesis: for b1 being M2(the carrier of T) holds
( not b1 is_<=_than X or b1 <= x `2 )
let y be Element of T; :: thesis: ( not y is_<=_than X or y <= x `2 )
assume A10:
y is_<=_than X
; :: thesis: y <= x `2
s <= s
;
then
s is_<=_than {s}
by YELLOW_0:7;
then
x >= [s,y]
by A8, A10, YELLOW_3:33;
hence
x `2 >= y
by A9, YELLOW_3:11; :: thesis: verum