let L be Lattice; :: thesis: for a, b being Element of L holds
( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
let a, b be Element of L; :: thesis: ( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )
consider c being Element of L such that
A1: c = a "/\" b ;
A2: for d being Element of (LattPOSet L) st d <= a % & d <= b % holds
c % >= d

proof

let d be Element of (LattPOSet L); :: thesis: ( d <= a % & d <= b % implies c % >= d )
assume that
A3: d <= a % and
A4: d <= b % ; :: thesis: c % >= d
A5: (% d) % = % d by LATTICE3:def 3
.= d by LATTICE3:def 4 ;
then A6: % d [= a by A3, LATTICE3:7;
A7: % d [= b by A4, A5, LATTICE3:7;
(% d) "/\" c = ((% d) "/\" a) "/\" b by A1, LATTICES:def 7
.= (% d) "/\" b by A6, LATTICES:4
.= % d by A7, LATTICES:4 ;
then % d [= c by LATTICES:4;
hence c % >= d by A5, LATTICE3:7; :: thesis: verum

end;

c [= b by A1, LATTICES:6;
then A8: c % <= b % by LATTICE3:7;
c [= a by A1, LATTICES:6;
then c % <= a % by LATTICE3:7;
then A9: c % = (a %) "/\" (b %) by A8, A2, YELLOW_0:23;
consider c being Element of L such that
A10: c = a "\/" b ;
A11: for d being Element of (LattPOSet L) st a % <= d & b % <= d holds
d >= c %

proof

let d be Element of (LattPOSet L); :: thesis: ( a % <= d & b % <= d implies d >= c % )
assume that
A12: a % <= d and
A13: b % <= d ; :: thesis: d >= c %
A14: (% d) % = % d by LATTICE3:def 3
.= d by LATTICE3:def 4 ;
then A15: a [= % d by A12, LATTICE3:7;
A16: b [= % d by A13, A14, LATTICE3:7;
(% d) "\/" c = ((% d) "\/" a) "\/" b by A10, LATTICES:def 5
.= (% d) "\/" b by A15, LATTICES:def 3
.= % d by A16, LATTICES:def 3 ;
then c [= % d by LATTICES:def 3;
hence d >= c % by A14, LATTICE3:7; :: thesis: verum

end;

b [= c by A10, LATTICES:5;
then A17: b % <= c % by LATTICE3:7;
a [= c by A10, LATTICES:5;
then a % <= c % by LATTICE3:7;
then c % = (a %) "\/" (b %) by A17, A11, YELLOW_0:22;
hence ( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) ) by A1, A9, A10, LATTICE3:def 3; :: thesis: verum