let X, Y be non empty reflexive RelStr ; ( [:X,Y:] is with_suprema implies ( X is with_suprema & Y is with_suprema ) )
assume A1:
[:X,Y:] is with_suprema
; ( X is with_suprema & Y is with_suprema )
A2:
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:]
by Def2;
thus
X is with_suprema
Y is with_suprema proof
let x,
y be
Element of
X;
LATTICE3:def 10 ex b1 being Element of the carrier of X st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of X holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
set a = the
Element of
Y;
A3:
the
Element of
Y <= the
Element of
Y
;
consider z being
Element of
[:X,Y:] such that A4:
(
[x, the Element of Y] <= z &
[y, the Element of Y] <= z )
and A5:
for
z9 being
Element of
[:X,Y:] st
[x, the Element of Y] <= z9 &
[y, the Element of Y] <= z9 holds
z <= z9
by A1;
take
z `1
;
( x <= z `1 & y <= z `1 & ( for b1 being Element of the carrier of X holds
( not x <= b1 or not y <= b1 or z `1 <= b1 ) ) )
A6:
z = [(z `1),(z `2)]
by A2, MCART_1:21;
hence
(
x <= z `1 &
y <= z `1 )
by A4, Th11;
for b1 being Element of the carrier of X holds
( not x <= b1 or not y <= b1 or z `1 <= b1 )
let z9 be
Element of
X;
( not x <= z9 or not y <= z9 or z `1 <= z9 )
assume
(
x <= z9 &
y <= z9 )
;
z `1 <= z9
then
(
[x, the Element of Y] <= [z9, the Element of Y] &
[y, the Element of Y] <= [z9, the Element of Y] )
by A3, Th11;
then
z <= [z9, the Element of Y]
by A5;
hence
z `1 <= z9
by A6, Th11;
verum
end;
set a = the Element of X;
A7:
the Element of X <= the Element of X
;
let x, y be Element of Y; LATTICE3:def 10 ex b1 being Element of the carrier of Y st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of Y holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
consider z being Element of [:X,Y:] such that
A8:
( [ the Element of X,x] <= z & [ the Element of X,y] <= z )
and
A9:
for z9 being Element of [:X,Y:] st [ the Element of X,x] <= z9 & [ the Element of X,y] <= z9 holds
z <= z9
by A1;
take
z `2
; ( x <= z `2 & y <= z `2 & ( for b1 being Element of the carrier of Y holds
( not x <= b1 or not y <= b1 or z `2 <= b1 ) ) )
A10:
z = [(z `1),(z `2)]
by A2, MCART_1:21;
hence
( x <= z `2 & y <= z `2 )
by A8, Th11; for b1 being Element of the carrier of Y holds
( not x <= b1 or not y <= b1 or z `2 <= b1 )
let z9 be Element of Y; ( not x <= z9 or not y <= z9 or z `2 <= z9 )
assume
( x <= z9 & y <= z9 )
; z `2 <= z9
then
( [ the Element of X,x] <= [ the Element of X,z9] & [ the Element of X,y] <= [ the Element of X,z9] )
by A7, Th11;
then
z <= [ the Element of X,z9]
by A9;
hence
z `2 <= z9
by A10, Th11; verum