let Y be set ; :: according to WELLFND1:def 2,WELLORD1:def 3 :: thesis: ( not Y c= the carrier of (LattPOSet L) or Y = {} or ex b₁ being set st
( b₁ in Y & the InternalRel of (LattPOSet L) -Seg b₁ misses Y ) )
set R = LattPOSet L;
assume that
A1: Y c= the carrier of (LattPOSet L) and
A2: Y <> {} ; :: thesis: ex b₁ being set st
( b₁ in Y & the InternalRel of (LattPOSet L) -Seg b₁ misses Y )
LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def 2;
then reconsider Y = Y as Subset of L by A1;
consider a being Element of (LattPOSet L) such that
A3: a in Y and
A4: for b being Element of (LattPOSet L) st b in Y & b <> a holds
not b <= a by A2, Lm1;
A5: for x being Element of (LattPOSet L) holds
( not x <> a or not [x,a] in the InternalRel of (LattPOSet L) or not x in Y )

proof

given x being Element of (LattPOSet L) such that A6: x <> a and
A7: [x,a] in the InternalRel of (LattPOSet L) and
A8: x in Y ; :: thesis: contradiction
x <= a by A7, ORDERS_2:def 5;
hence contradiction by A4, A6, A8; :: thesis: verum

end;

( the InternalRel of (LattPOSet L) -Seg a) /\ Y = {}

proof

set z = the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y;
assume A9: ( the InternalRel of (LattPOSet L) -Seg a) /\ Y <> {} ; :: thesis: contradiction
then the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y in the InternalRel of (LattPOSet L) -Seg a by XBOOLE_0:def 4;
then A10: ( the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y <> a & [ the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y,a] in the InternalRel of (LattPOSet L) ) by WELLORD1:1;
the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y in Y by A9, XBOOLE_0:def 4;
hence contradiction by A1, A5, A10; :: thesis: verum

end;

then the InternalRel of (LattPOSet L) -Seg a misses Y by XBOOLE_0:def 7;
hence ex b₁ being set st
( b₁ in Y & the InternalRel of (LattPOSet L) -Seg b₁ misses Y ) by A3; :: thesis: verum