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 that
A1: the InternalRel of L -Seg a misses Y and
A2: a in Y ; :: thesis: a is_minimal_wrt Y, the InternalRel of L
A3: ( the InternalRel of L -Seg a) /\ Y = {} by A1, XBOOLE_0:def 7;
now :: thesis: for y being set holds
( not y in Y or not y <> a or not [y,a] in the InternalRel of L )
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
A4: y in Y and
A5: y <> a and
A6: [y,a] in the InternalRel of L ;
y in the InternalRel of L -Seg a by A5, A6, WELLORD1:1;
hence contradiction by A3, A4, XBOOLE_0:def 4; :: thesis: verum
end;
hence a is_minimal_wrt Y, the InternalRel of L by A2, WAYBEL_4:def 25; :: thesis: verum
end;
assume A7: a is_minimal_wrt Y, the InternalRel of L ; :: thesis: ( the InternalRel of L -Seg a misses Y & a in Y )
now :: thesis: the InternalRel of L -Seg a misses Y
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 object such that
A8: y in ( the InternalRel of L -Seg a) /\ Y by XBOOLE_0:def 1;
A9: y in the InternalRel of L -Seg a by A8, XBOOLE_0:def 4;
A10: y in Y by A8, XBOOLE_0:def 4;
A11: y <> a by A9, WELLORD1:1;
[y,a] in the InternalRel of L by A9, WELLORD1:1;
hence contradiction by A7, A10, A11, WAYBEL_4:def 25; :: thesis: verum
end;
hence the InternalRel of L -Seg a misses Y ; :: thesis: a in Y
thus a in Y by A7, WAYBEL_4:def 25; :: thesis: verum