Theorem dlatl

Description: A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Assertion	dlatl	|- ( K e. DLat -> K e. Lat )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` K ) = ( Base ` K )
2		eqid	|- ( join ` K ) = ( join ` K )
3		eqid	|- ( meet ` K ) = ( meet ` K )
4	1 2 3	isdlat	|- ( K e. DLat <-> ( K e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( meet ` K ) ( y ( join ` K ) z ) ) = ( ( x ( meet ` K ) y ) ( join ` K ) ( x ( meet ` K ) z ) ) ) )
5	4	simplbi	|- ( K e. DLat -> K e. Lat )