let A be set ; :: thesis: for a, b being Element of (EqRelLATT A) holds
( a <= b iff a c= b )
let a, b be Element of (EqRelLATT A); :: thesis: ( a <= b iff a c= b )
set El = EqRelLatt A;
reconsider a9 = a as Element of (EqRelLatt A) ;
reconsider b9 = b as Element of (EqRelLatt A) ;
thus ( a <= b implies a c= b ) :: thesis: ( a c= b implies a <= b )
proof
assume a <= b ; :: thesis: a c= b
then a9 % <= b9 % ;
then a9 [= b9 by LATTICE3:7;
hence a c= b by Th5; :: thesis: verum
end;
thus ( a c= b implies a <= b ) :: thesis: verum
proof
assume a c= b ; :: thesis: a <= b
then a9 [= b9 by Th5;
then a9 % <= b9 % by LATTICE3:7;
hence a <= b ; :: thesis: verum
end;