let L be WA-Lattice; :: thesis: for a, b being Element of L
for aa, bb being Element of (wlatt 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 (wlatt L) st a = aa & b = bb holds
( aa [= bb iff a <= b )
let aa, bb be Element of (wlatt 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: LatRelStr (wlatt L) = RelStr(# the carrier of L, the InternalRel of L #) by WLatDef;
thus ( aa [= bb implies a <= b ) :: thesis: ( a <= b implies aa [= bb )

proof

assume aa [= bb ; :: thesis: a <= b
then consider xx, yy being Element of (wlatt L) such that
A1: ( [aa,bb] = [xx,yy] & xx [= yy ) ;
[a,b] in { [x,y] where x, y is Element of (wlatt L) : x [= y } by AA, A1;
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 consider xx, yy being Element of (wlatt L) such that
A1: ( [a,b] = [xx,yy] & xx [= yy ) by WW;
( a = xx & b = yy ) by XTUPLE_0:1, A1;
hence aa [= bb by A1, AA; :: thesis: verum