let L be non empty transitive antisymmetric RelStr ; for x being Element of L
for a, N being set st a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L holds
a is_minimal_wrt N, the InternalRel of L
let x be Element of L; for a, N being set st a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L holds
a is_minimal_wrt N, the InternalRel of L
let a, N be set ; ( a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L implies a is_minimal_wrt N, the InternalRel of L )
assume A1:
a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L
; a is_minimal_wrt N, the InternalRel of L
set IR = the InternalRel of L;
set CR = the carrier of L;
A2:
the InternalRel of L is_transitive_in the carrier of L
by ORDERS_2:def 3;
hence
a is_minimal_wrt N, the InternalRel of L
by WAYBEL_4:def 25; verum