set LL = LatRelStr L;
thus LatRelStr L is with_suprema :: thesis: LatRelStr L is with_infima

proof

let x, y be Element of (LatRelStr L); :: according to LATTICE3:def 10 :: thesis: ex b₁ being Element of the carrier of (LatRelStr L) st
( x <= b₁ & y <= b₁ & ( for b₂ being Element of the carrier of (LatRelStr L) holds
( not x <= b₂ or not y <= b₂ or b₁ <= b₂ ) ) )
reconsider xx = x, yy = y as Element of L ;
reconsider z = xx "\/" yy as Element of (LatRelStr L) ;
take z ; :: thesis: ( x <= z & y <= z & ( for b₁ being Element of the carrier of (LatRelStr L) holds
( not x <= b₁ or not y <= b₁ or z <= b₁ ) ) )
A1: xx [= xx "\/" yy by LATWAL_1:9;
yy [= yy "\/" xx by LATWAL_1:9;
hence ( x <= z & y <= z ) by A1, LemmaEqual0; :: thesis: for b₁ being Element of the carrier of (LatRelStr L) holds
( not x <= b₁ or not y <= b₁ or z <= b₁ )
let z9 be Element of (LatRelStr L); :: thesis: ( not x <= z9 or not y <= z9 or z <= z9 )
reconsider zz9 = z9 as Element of L ;
reconsider zzz9 = zz9 as Element of (LatRelStr L) ;
assume that
A6: x <= z9 and
A7: y <= z9 ; :: thesis: z <= z9
A8: % x [= zz9 by A6, LemmaEqual0;
% y [= % z9 by A7, LemmaEqual0;
then (% x) "\/" (% y) [= % z9 by A8, LATWAL_1:11;
hence z <= z9 by LemmaEqual0; :: thesis: verum

end;

let x, y be Element of (LatRelStr L); :: according to LATTICE3:def 11 :: thesis: ex b₁ being Element of the carrier of (LatRelStr L) st
( b₁ <= x & b₁ <= y & ( for b₂ being Element of the carrier of (LatRelStr L) holds
( not b₂ <= x or not b₂ <= y or b₂ <= b₁ ) ) )
take z = ((% x) "/\" (% y)) % ; :: thesis: ( z <= x & z <= y & ( for b₁ being Element of the carrier of (LatRelStr L) holds
( not b₁ <= x or not b₁ <= y or b₁ <= z ) ) )
A9: (% x) "/\" (% y) [= % x by LATTICES:6;
(% y) "/\" (% x) [= % y by LATTICES:6;
hence ( z <= x & z <= y ) by A9, LemmaEqual0; :: thesis: for b₁ being Element of the carrier of (LatRelStr L) holds
( not b₁ <= x or not b₁ <= y or b₁ <= z )
let z9 be Element of (LatRelStr L); :: thesis: ( not z9 <= x or not z9 <= y or z9 <= z )
assume that
A14: z9 <= x and
A15: z9 <= y ; :: thesis: z9 <= z
A16: % z9 [= % x by A14, LemmaEqual0;
% z9 [= % y by A15, LemmaEqual0;
then % z9 [= (% x) "/\" (% y) by A16, LATWAL_1:13;
hence z9 <= z by LemmaEqual0; :: thesis: verum