let R1, R2 be non empty RelStr ; ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE implies R2 is LATTICE )
assume that
A1:
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
and
A2:
R1 is LATTICE
; R2 is LATTICE
A3:
R2 is with_infima
proof
let x,
y be
Element of
R2;
LATTICE3:def 11 ex b1 being Element of the carrier of R2 st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of R2 holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
reconsider x9 =
x,
y9 =
y as
Element of
R1 by A1;
consider z9 being
Element of
R1 such that A4:
z9 <= x9
and A5:
z9 <= y9
and A6:
for
w9 being
Element of
R1 st
w9 <= x9 &
w9 <= y9 holds
w9 <= z9
by A2, LATTICE3:def 11;
reconsider z =
z9 as
Element of
R2 by A1;
take
z
;
( z <= x & z <= y & ( for b1 being Element of the carrier of R2 holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
thus
(
z <= x &
z <= y )
by A1, A4, A5, Lm1;
for b1 being Element of the carrier of R2 holds
( not b1 <= x or not b1 <= y or b1 <= z )
let w be
Element of
R2;
( not w <= x or not w <= y or w <= z )
reconsider w9 =
w as
Element of
R1 by A1;
assume that A7:
w <= x
and A8:
w <= y
;
w <= z
A9:
w9 <= x9
by A1, A7, Lm1;
w9 <= y9
by A1, A8, Lm1;
then
w9 <= z9
by A6, A9;
hence
w <= z
by A1, Lm1;
verum
end;
A10:
R2 is with_suprema
proof
let x,
y be
Element of
R2;
LATTICE3:def 10 ex b1 being Element of the carrier of R2 st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of R2 holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
reconsider x9 =
x,
y9 =
y as
Element of
R1 by A1;
consider z9 being
Element of
R1 such that A11:
z9 >= x9
and A12:
z9 >= y9
and A13:
for
w9 being
Element of
R1 st
w9 >= x9 &
w9 >= y9 holds
w9 >= z9
by A2, LATTICE3:def 10;
reconsider z =
z9 as
Element of
R2 by A1;
take
z
;
( x <= z & y <= z & ( for b1 being Element of the carrier of R2 holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
thus
(
z >= x &
z >= y )
by A1, A11, A12, Lm1;
for b1 being Element of the carrier of R2 holds
( not x <= b1 or not y <= b1 or z <= b1 )
let w be
Element of
R2;
( not x <= w or not y <= w or z <= w )
reconsider w9 =
w as
Element of
R1 by A1;
assume that A14:
w >= x
and A15:
w >= y
;
z <= w
A16:
w9 >= x9
by A1, A14, Lm1;
w9 >= y9
by A1, A15, Lm1;
then
w9 >= z9
by A13, A16;
hence
z <= w
by A1, Lm1;
verum
end;
A17:
R2 is reflexive
by A1, A2, YELLOW_0:def 1, Lm1;
A18:
R2 is transitive
proof
let x,
y,
z be
Element of
R2;
YELLOW_0:def 2 ( not x <= y or not y <= z or x <= z )
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
R1 by A1;
assume that A19:
x <= y
and A20:
y <= z
;
x <= z
A21:
x9 <= y9
by A1, A19, Lm1;
y9 <= z9
by A1, A20, Lm1;
then
x9 <= z9
by A2, A21, YELLOW_0:def 2;
hence
x <= z
by A1, Lm1;
verum
end;
R2 is antisymmetric
hence
R2 is LATTICE
by A3, A10, A17, A18; verum