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 ;
( c [= a & c [= b ) by A1, LATTICES:23;
then A2: ( c % <= a % & c % <= b % ) by LATTICE3:7;
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 A3: ( d <= a % & d <= b % ) ; :: thesis: c % >= d
A4: (% d) % = % d by LATTICE3:def 3
.= d by LATTICE3:def 4 ;
then A5: ( % d [= a & % d [= b ) by A3, LATTICE3:7;
(% d) "/\" c = ((% d) "/\" a) "/\" b by A1, LATTICES:def 7
.= (% d) "/\" b by A5, LATTICES:21
.= % d by A5, LATTICES:21 ;
then % d [= c by LATTICES:21;
hence c % >= d by A4, LATTICE3:7; :: thesis: verum

end;

then A6: c % = (a % ) "/\" (b % ) by A2, YELLOW_0:23;
consider c being Element of L such that
A7: c = a "\/" b ;
( a [= c & b [= c ) by A7, LATTICES:22;
then A8: ( a % <= c % & b % <= c % ) by LATTICE3:7;
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 A9: ( a % <= d & b % <= d ) ; :: thesis: d >= c %
A10: (% d) % = % d by LATTICE3:def 3
.= d by LATTICE3:def 4 ;
then A11: ( a [= % d & b [= % d ) by A9, LATTICE3:7;
(% d) "\/" c = ((% d) "\/" a) "\/" b by A7, LATTICES:def 5
.= (% d) "\/" b by A11, LATTICES:def 3
.= % d by A11, LATTICES:def 3 ;
then c [= % d by LATTICES:def 3;
hence d >= c % by A10, LATTICE3:7; :: thesis: verum

end;

then c % = (a % ) "\/" (b % ) by A8, YELLOW_0:22;
hence ( a "/\" b = (a % ) "/\" (b % ) & a "\/" b = (a % ) "\/" (b % ) ) by A1, A6, A7, LATTICE3:def 3; :: thesis: verum