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 ) )

reconsider xy = x "\/" y as Element of B_6 by Th9, YELLOW_1:1;

assume that

A1: a = x and

A2: b = y ; :: thesis: ( a "\/" b = x "\/" y & a "/\" b = x "/\" y )

x [= x "\/" y by LATTICES:5;

then A3: a <= xy by A1, Th13;

A4: for d being Element of B_6 st d >= a & d >= b holds

xy <= d

then A5: b <= xy by A2, Th13;

reconsider xy = x "/\" y as Element of B_6 by Th9, YELLOW_1:1;

x "/\" y [= y by LATTICES:6;

then A6: xy <= b by A2, Th13;

A7: for d being Element of B_6 st d <= a & d <= b holds

xy >= d

then xy <= a by A1, Th13;

hence ( a "\/" b = x "\/" y & a "/\" b = x "/\" y ) by A3, A5, A4, A6, A7, YELLOW_0:22, YELLOW_0:23; :: thesis: verum

( 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 ) )

reconsider xy = x "\/" y as Element of B_6 by Th9, YELLOW_1:1;

assume that

A1: a = x and

A2: b = y ; :: thesis: ( a "\/" b = x "\/" y & a "/\" b = x "/\" y )

x [= x "\/" y by LATTICES:5;

then A3: a <= xy by A1, Th13;

A4: for d being Element of B_6 st d >= a & d >= b holds

xy <= d

proof

y [= x "\/" y
by LATTICES:5;
let d be Element of B_6; :: thesis: ( d >= a & d >= b implies xy <= d )

reconsider e = d as Element of Benzene by Th9, YELLOW_1:1;

assume ( d >= a & d >= b ) ; :: thesis: xy <= d

then ( x [= e & y [= e ) by A1, A2, Th13;

then x "\/" y [= e by FILTER_0:6;

hence xy <= d by Th13; :: thesis: verum

end;reconsider e = d as Element of Benzene by Th9, YELLOW_1:1;

assume ( d >= a & d >= b ) ; :: thesis: xy <= d

then ( x [= e & y [= e ) by A1, A2, Th13;

then x "\/" y [= e by FILTER_0:6;

hence xy <= d by Th13; :: thesis: verum

then A5: b <= xy by A2, Th13;

reconsider xy = x "/\" y as Element of B_6 by Th9, YELLOW_1:1;

x "/\" y [= y by LATTICES:6;

then A6: xy <= b by A2, Th13;

A7: for d being Element of B_6 st d <= a & d <= b holds

xy >= d

proof

x "/\" y [= x
by LATTICES:6;
let d be Element of B_6; :: thesis: ( d <= a & d <= b implies xy >= d )

reconsider e = d as Element of Benzene by Th9, YELLOW_1:1;

assume ( d <= a & d <= b ) ; :: thesis: xy >= d

then ( e [= x & e [= y ) by A1, A2, Th13;

then e [= x "/\" y by FILTER_0:7;

hence xy >= d by Th13; :: thesis: verum

end;reconsider e = d as Element of Benzene by Th9, YELLOW_1:1;

assume ( d <= a & d <= b ) ; :: thesis: xy >= d

then ( e [= x & e [= y ) by A1, A2, Th13;

then e [= x "/\" y by FILTER_0:7;

hence xy >= d by Th13; :: thesis: verum

then xy <= a by A1, Th13;

hence ( a "\/" b = x "\/" y & a "/\" b = x "/\" y ) by A3, A5, A4, A6, A7, YELLOW_0:22, YELLOW_0:23; :: thesis: verum