let a, b be Element of B_6 ; :: thesis: for x, y being Element of Benzene st a = x & b = y holds
( a "\/" b = x "\/" y & a "/\" b = x "/\" y )
let x, y be Element of Benzene ; :: thesis: ( a = x & b = y implies ( a "\/" b = x "\/" y & a "/\" b = x "/\" y ) )
assume X0: ( a = x & b = y ) ; :: thesis: ( a "\/" b = x "\/" y & a "/\" b = x "/\" y )
reconsider xy = x "\/" y as Element of B_6 by LemBen, YELLOW_1:1;
( x [= x "\/" y & y [= x "\/" y ) by LATTICES:22;
then X1: ( a <= xy & b <= xy ) by X0, HiHi;
t1: for d being Element of B_6 st d >= a & d >= b holds
xy <= d

proof

let d be Element of B_6 ; :: thesis: ( d >= a & d >= b implies xy <= d )
reconsider e = d as Element of Benzene by LemBen, YELLOW_1:1;
assume ( d >= a & d >= b ) ; :: thesis: xy <= d
then ( x [= e & y [= e ) by X0, HiHi;
then x "\/" y [= e by FILTER_0:6;
hence xy <= d by HiHi; :: thesis: verum

end;

reconsider xy = x "/\" y as Element of B_6 by LemBen, YELLOW_1:1;
( x "/\" y [= x & x "/\" y [= y ) by LATTICES:23;
then x1: ( xy <= a & xy <= b ) by X0, HiHi;
for d being Element of B_6 st d <= a & d <= b holds
xy >= d

proof

let d be Element of B_6 ; :: thesis: ( d <= a & d <= b implies xy >= d )
reconsider e = d as Element of Benzene by LemBen, YELLOW_1:1;
assume ( d <= a & d <= b ) ; :: thesis: xy >= d
then ( e [= x & e [= y ) by X0, HiHi;
then e [= x "/\" y by FILTER_0:7;
hence xy >= d by HiHi; :: thesis: verum

end;

hence ( a "\/" b = x "\/" y & a "/\" b = x "/\" y ) by t1, X1, x1, YELLOW_0:22, YELLOW_0:23; :: thesis: verum