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
proof
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;
y [= x "\/" y by LATTICES:5;
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
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;
x "/\" y [= x by LATTICES:6;
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