Theorem ople1

Description: Any element is less than the orthoposet unit. ( chss analog.) (Contributed by NM, 23-Oct-2011)

	Ref	Expression
Hypotheses	ople1.b	|- B = ( Base ` K )
	ople1.l	|- .<_ = ( le ` K )
	ople1.u	|- .1. = ( 1. ` K )
Assertion	ople1	|- ( ( K e. OP /\ X e. B ) -> X .<_ .1. )

Proof

Step	Hyp	Ref	Expression
1		ople1.b	|- B = ( Base ` K )
2		ople1.l	|- .<_ = ( le ` K )
3		ople1.u	|- .1. = ( 1. ` K )
4		eqid	|- ( lub ` K ) = ( lub ` K )
5		simpl	|- ( ( K e. OP /\ X e. B ) -> K e. OP )
6		simpr	|- ( ( K e. OP /\ X e. B ) -> X e. B )
7		eqid	|- ( glb ` K ) = ( glb ` K )
8	1 4 7	op01dm	|- ( K e. OP -> ( B e. dom ( lub ` K ) /\ B e. dom ( glb ` K ) ) )
9	8	simpld	|- ( K e. OP -> B e. dom ( lub ` K ) )
10	9	adantr	|- ( ( K e. OP /\ X e. B ) -> B e. dom ( lub ` K ) )
11	1 4 2 3 5 6 10	ple1	|- ( ( K e. OP /\ X e. B ) -> X .<_ .1. )