set R = LattPOSet L;
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 ) )
assume A1: ( Y c= the carrier of (LattPOSet L) & 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
A2: ( a in Y & ( for b being Element of (LattPOSet L) st b in Y & b <> a holds
not b <= a ) ) by A1, Lm1;
A3: 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 A4: ( x <> a & [x,a] in the InternalRel of (LattPOSet L) & x in Y ) ; :: thesis: contradiction
x <= a by A4, ORDERS_2:def 9;
hence contradiction by A2, A4; :: thesis: verum

end;

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

proof

assume A5: (the InternalRel of (LattPOSet L) -Seg a) /\ Y <> {} ; :: thesis: contradiction
consider z being Element of (the InternalRel of (LattPOSet L) -Seg a) /\ Y;
A6: ( z in the InternalRel of (LattPOSet L) -Seg a & z in Y ) by A5, XBOOLE_0:def 4;
then ( z <> a & [z,a] in the InternalRel of (LattPOSet L) ) by WELLORD1:def 1;
hence contradiction by A1, A3, A6; :: 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 A2; :: thesis: verum