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 )
hereby :: thesis: ( x [= y implies a <= b )
assume a <= b ; :: thesis: x [= y
then x % <= y % by A1, Th1, Th12;
hence x [= y by LATTICE3:7; :: thesis: verum
end;
assume x [= y ; :: thesis: a <= b
then x % <= y % by LATTICE3:7;
hence a <= b by A1, Th1, Th12; :: thesis: verum