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 ; :: 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 by A1;
consider z' being Element of such that
A4: z' <= x' and
A5: z' <= y' and
A6: for w' being Element of st w' <= x' & w' <= y' holds
w' <= z' by A2, LATTICE3:def 11;
reconsider z = z' as Element of 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, A5, 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 ; :: thesis: ( not w <= x or not w <= y or w <= z )
reconsider w' = w as Element of by A1;
assume that
A7: w <= x and
A8: w <= y ; :: thesis: w <= z
A9: w' <= x' by A1, A7, Lm1;
w' <= y' by A1, A8, Lm1;
then w' <= z' by A6, A9;
hence w <= z by A1, Lm1; :: thesis: verum

end;

A10: R2 is with_suprema

proof

let x, y be Element of ; :: 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 by A1;
consider z' being Element of such that
A11: z' >= x' and
A12: z' >= y' and
A13: for w' being Element of st w' >= x' & w' >= y' holds
w' >= z' by A2, LATTICE3:def 10;
reconsider z = z' as Element of 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, A11, A12, 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 ; :: thesis: ( not x <= w or not y <= w or z <= w )
reconsider w' = w as Element of by A1;
assume that
A14: w >= x and
A15: w >= y ; :: thesis: z <= w
A16: w' >= x' by A1, A14, Lm1;
w' >= y' by A1, A15, Lm1;
then w' >= z' by A13, A16;
hence z <= w by A1, Lm1; :: thesis: verum

end;

A17: R2 is reflexive

proof

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

end;

A18: R2 is transitive

proof

let x, y, z be Element of ; :: 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 by A1;
assume that
A19: x <= y and
A20: y <= z ; :: thesis: x <= z
A21: x' <= y' by A1, A19, Lm1;
y' <= z' by A1, A20, Lm1;
then x' <= z' by A2, A21, YELLOW_0:def 2;
hence x <= z by A1, Lm1; :: thesis: verum

end;

R2 is antisymmetric

proof

let x, y be Element of ; :: 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 by A1;
assume that
A22: x <= y and
A23: y <= x ; :: thesis: x = y
A24: x' <= y' by A1, A22, Lm1;
y' <= x' by A1, A23, Lm1;
hence x = y by A2, A24, YELLOW_0:def 3; :: thesis: verum

end;

hence R2 is LATTICE by A3, A10, A17, A18; :: thesis: verum