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