let L be with_suprema with_infima Poset; :: thesis: for a, b being Element of L
for aa, bb being Element of (latt L) st a = aa & b = bb holds
( aa [= bb iff a <= b )
let a, b be Element of L; :: thesis: for aa, bb being Element of (latt L) st a = aa & b = bb holds
( aa [= bb iff a <= b )
let aa, bb be Element of (latt L); :: thesis: ( a = aa & b = bb implies ( aa [= bb iff a <= b ) )
assume AA: ( a = aa & b = bb ) ; :: thesis: ( aa [= bb iff a <= b )
WW: LattPOSet (latt L) = RelStr(# the carrier of L, the InternalRel of L #) by LATTICE3:def 15;
thus ( aa [= bb implies a <= b ) :: thesis: ( a <= b implies aa [= bb )

proof

assume aa [= bb ; :: thesis: a <= b
then [aa,bb] in LatOrder (latt L) ;
then [a,b] in LattRel (latt L) by AA, Eq0;
hence a <= b by WW, ORDERS_2:def 5; :: thesis: verum

end;

assume a <= b ; :: thesis: aa [= bb
then [a,b] in the InternalRel of L by ORDERS_2:def 5;
then [a,b] in { [x,y] where x, y is Element of (latt L) : x [= y } by WW, FILTER_1:def 8;
then consider xx, yy being Element of (latt L) such that
A1: ( [a,b] = [xx,yy] & xx [= yy ) ;
( a = xx & b = yy ) by XTUPLE_0:1, A1;
hence aa [= bb by A1, AA; :: thesis: verum