let L be Lattice; :: thesis: LattRel L = LatOrder L
LattRel L = LatOrder L

proof

T1: LattRel L c= LatOrder L

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in LattRel L or [x,y] in LatOrder L )
assume [x,y] in LattRel L ; :: thesis: [x,y] in LatOrder L
then [x,y] in { [xx,yy] where xx, yy is Element of L : xx [= yy } by FILTER_1:def 8;
then consider xx, yy being Element of L such that
ZZ: ( [xx,yy] = [x,y] & xx [= yy ) ;
thus [x,y] in LatOrder L by ZZ; :: thesis: verum

end;

LatOrder L c= LattRel L

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in LatOrder L or [x,y] in LattRel L )
assume [x,y] in LatOrder L ; :: thesis: [x,y] in LattRel L
then consider xx, yy being Element of L such that
ZZ: ( [xx,yy] = [x,y] & xx [= yy ) ;
[x,y] in { [x1,y1] where x1, y1 is Element of L : x1 [= y1 } by ZZ;
hence [x,y] in LattRel L by FILTER_1:def 8; :: thesis: verum

end;

hence LattRel L = LatOrder L by T1, XBOOLE_0:def 10; :: thesis: verum

end;

hence LattRel L = LatOrder L ; :: thesis: verum