let a, b be Element of B_6; :: thesis: for x, y being Element of Benzene st a = x & b = y holds

( a <= b iff x [= y )

let x, y be Element of Benzene; :: thesis: ( a = x & b = y implies ( a <= b iff x [= y ) )

assume A1: ( a = x & b = y ) ; :: thesis: ( a <= b iff x [= y )

then x % <= y % by LATTICE3:7;

hence a <= b by A1, Th1, Th12; :: thesis: verum

( a <= b iff x [= y )

let x, y be Element of Benzene; :: thesis: ( a = x & b = y implies ( a <= b iff x [= y ) )

assume A1: ( a = x & b = y ) ; :: thesis: ( a <= b iff x [= y )

hereby :: thesis: ( x [= y implies a <= b )

assume
x [= y
; :: thesis: a <= bassume
a <= b
; :: thesis: x [= y

then x % <= y % by A1, Th1, Th12;

hence x [= y by LATTICE3:7; :: thesis: verum

end;then x % <= y % by A1, Th1, Th12;

hence x [= y by LATTICE3:7; :: thesis: verum

then x % <= y % by LATTICE3:7;

hence a <= b by A1, Th1, Th12; :: thesis: verum