let L be RelStr ; :: thesis: for Y, a being set holds
( ( the InternalRel of L -Seg a misses Y & a in Y ) iff a is_minimal_wrt Y,the InternalRel of L )
let Y, a be set ; :: thesis: ( ( the InternalRel of L -Seg a misses Y & a in Y ) iff a is_minimal_wrt Y,the InternalRel of L )
set IR = the InternalRel of L;

hereby :: thesis: ( a is_minimal_wrt Y,the InternalRel of L implies ( the InternalRel of L -Seg a misses Y & a in Y ) )

assume A1: ( the InternalRel of L -Seg a misses Y & a in Y ) ; :: thesis: a is_minimal_wrt Y,the InternalRel of L
then A2: (the InternalRel of L -Seg a) /\ Y = {} by XBOOLE_0:def 7;

now

thus a in Y by A1; :: thesis: for y being set holds
( not y in Y or not y <> a or not [y,a] in the InternalRel of L )

now

assume ex y being set st
( y in Y & y <> a & [y,a] in the InternalRel of L ) ; :: thesis: contradiction
then consider y being set such that
A3: ( y in Y & y <> a & [y,a] in the InternalRel of L ) ;
y in the InternalRel of L -Seg a by A3, WELLORD1:def 1;
hence contradiction by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;

hence for y being set holds
( not y in Y or not y <> a or not [y,a] in the InternalRel of L ) ; :: thesis: verum

end;

hence a is_minimal_wrt Y,the InternalRel of L by WAYBEL_4:def 26; :: thesis: verum

end;

assume A4: a is_minimal_wrt Y,the InternalRel of L ; :: thesis: ( the InternalRel of L -Seg a misses Y & a in Y )

now

assume not the InternalRel of L -Seg a misses Y ; :: thesis: contradiction
then (the InternalRel of L -Seg a) /\ Y <> {} by XBOOLE_0:def 7;
then consider y being set such that
A5: y in (the InternalRel of L -Seg a) /\ Y by XBOOLE_0:def 1;
A6: ( y in the InternalRel of L -Seg a & y in Y ) by A5, XBOOLE_0:def 4;
then ( y <> a & [y,a] in the InternalRel of L ) by WELLORD1:def 1;
hence contradiction by A4, A6, WAYBEL_4:def 26; :: thesis: verum

end;

hence the InternalRel of L -Seg a misses Y ; :: thesis: a in Y
thus a in Y by A4, WAYBEL_4:def 26; :: thesis: verum