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 b1 being object st
( b1 in Y & the InternalRel of (LattPOSet L) -Seg b1 misses Y ) )
set R = LattPOSet L;
assume that
A1: Y c= the carrier of (LattPOSet L) and
A2: Y <> {} ; :: thesis: ex b1 being object st
( b1 in Y & the InternalRel of (LattPOSet L) -Seg b1 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 ) by ORDERS_2:def 5, A4;
( the InternalRel of (LattPOSet L) -Seg a) /\ Y = {}
proof
set z = the Element of ( the InternalRel of (LattPOSet L) -Seg a) /\ Y;
assume A6: ( 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 A7: ( 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 A6, XBOOLE_0:def 4;
hence contradiction by A1, A5, A7; :: thesis: verum
end;
then the InternalRel of (LattPOSet L) -Seg a misses Y by XBOOLE_0:def 7;
hence ex b1 being object st
( b1 in Y & the InternalRel of (LattPOSet L) -Seg b1 misses Y ) by A3; :: thesis: verum