let R1, R2 be non empty RelStr ; :: thesis: ( 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 ; :: thesis: R2 is LATTICE
A3: R2 is with_infima

proof

let x, y be Element of R2; :: according to LATTICE3:def 11 :: thesis: ex b₁ being Element of the carrier of R2 st
( b₁ <= x & b₁ <= y & ( for b₂ being Element of the carrier of R2 holds
( not b₂ <= x or not b₂ <= y or b₂ <= b₁ ) ) )
reconsider x' = x, y' = y as Element of R1 by A1;
consider z' being Element of R1 such that
A4: ( z' <= x' & z' <= y' ) and
A5: for w' being Element of R1 st w' <= x' & w' <= y' holds
w' <= z' by A2, LATTICE3:def 11;
reconsider z = z' as Element of R2 by A1;
take z ; :: thesis: ( z <= x & z <= y & ( for b₁ being Element of the carrier of R2 holds
( not b₁ <= x or not b₁ <= y or b₁ <= z ) ) )
thus ( z <= x & z <= y ) by A1, A4, Lm1; :: thesis: for b₁ being Element of the carrier of R2 holds
( not b₁ <= x or not b₁ <= y or b₁ <= z )
let w be Element of R2; :: thesis: ( not w <= x or not w <= y or w <= z )
reconsider w' = w as Element of R1 by A1;
assume ( w <= x & w <= y ) ; :: thesis: w <= z
then ( w' <= x' & w' <= y' ) by A1, Lm1;
then w' <= z' by A5;
hence w <= z by A1, Lm1; :: thesis: verum

end;

A6: R2 is with_suprema

proof

let x, y be Element of R2; :: according to LATTICE3:def 10 :: thesis: ex b₁ being Element of the carrier of R2 st
( x <= b₁ & y <= b₁ & ( for b₂ being Element of the carrier of R2 holds
( not x <= b₂ or not y <= b₂ or b₁ <= b₂ ) ) )
reconsider x' = x, y' = y as Element of R1 by A1;
consider z' being Element of R1 such that
A7: ( z' >= x' & z' >= y' ) and
A8: for w' being Element of R1 st w' >= x' & w' >= y' holds
w' >= z' by A2, LATTICE3:def 10;
reconsider z = z' as Element of R2 by A1;
take z ; :: thesis: ( x <= z & y <= z & ( for b₁ being Element of the carrier of R2 holds
( not x <= b₁ or not y <= b₁ or z <= b₁ ) ) )
thus ( z >= x & z >= y ) by A1, A7, Lm1; :: thesis: for b₁ being Element of the carrier of R2 holds
( not x <= b₁ or not y <= b₁ or z <= b₁ )
let w be Element of R2; :: thesis: ( not x <= w or not y <= w or z <= w )
reconsider w' = w as Element of R1 by A1;
assume ( w >= x & w >= y ) ; :: thesis: z <= w
then ( w' >= x' & w' >= y' ) by A1, Lm1;
then w' >= z' by A8;
hence z <= w by A1, Lm1; :: thesis: verum

end;

A9: R2 is reflexive

proof

let x be Element of R2; :: according to YELLOW_0:def 1 :: thesis: x <= x
reconsider x' = x as Element of R1 by A1;
x' <= x' by A2, YELLOW_0:def 1;
hence x <= x by A1, Lm1; :: thesis: verum

end;

A10: R2 is transitive

proof

let x, y, z be Element of R2; :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
reconsider x' = x, y' = y, z' = z as Element of R1 by A1;
assume ( x <= y & y <= z ) ; :: thesis: x <= z
then ( x' <= y' & y' <= z' ) by A1, Lm1;
then x' <= z' by A2, YELLOW_0:def 2;
hence x <= z by A1, Lm1; :: thesis: verum

end;

R2 is antisymmetric

proof

let x, y be Element of R2; :: according to YELLOW_0:def 3 :: thesis: ( not x <= y or not y <= x or x = y )
reconsider x' = x, y' = y as Element of R1 by A1;
assume ( x <= y & y <= x ) ; :: thesis: x = y
then ( x' <= y' & y' <= x' ) by A1, Lm1;
hence x = y by A2, YELLOW_0:def 3; :: thesis: verum

end;

hence R2 is LATTICE by A3, A6, A9, A10; :: thesis: verum