Theorem islln4

Description: The predicate "is a lattice line". (Contributed by NM, 16-Jun-2012)

	Ref	Expression
Hypotheses	llnset.b	$$⊢B={\mathrm{Base}}_K$$
	llnset.c	$$⊢C={⋖}_K$$
	llnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	llnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
Assertion	islln4	$$⊢\left(K\in D\wedge X\in B\right)\to \left(X\in N\leftrightarrow \exists p\in ApCX\right)$$

Proof

Step	Hyp	Ref	Expression
1		llnset.b	$$⊢B={\mathrm{Base}}_K$$
2		llnset.c	$$⊢C={⋖}_K$$
3		llnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		llnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
5	1 2 3 4	islln	$$⊢K\in D\to \left(X\in N\leftrightarrow \left(X\in B\wedge \exists p\in ApCX\right)\right)$$
6	5	baibd	$$⊢\left(K\in D\wedge X\in B\right)\to \left(X\in N\leftrightarrow \exists p\in ApCX\right)$$