let A be non empty RelStr ; for B being Subset of A
for a1, a2 being Element of A st the InternalRel of A is_connected_in B & a1 in B & a2 in B & a1 <> a2 & not a1 <= a2 holds
a2 <= a1
let B be Subset of A; for a1, a2 being Element of A st the InternalRel of A is_connected_in B & a1 in B & a2 in B & a1 <> a2 & not a1 <= a2 holds
a2 <= a1
let a1, a2 be Element of A; ( the InternalRel of A is_connected_in B & a1 in B & a2 in B & a1 <> a2 & not a1 <= a2 implies a2 <= a1 )
assume that
A1:
the InternalRel of A is_connected_in B
and
A2:
a1 in B
and
A3:
a2 in B
and
A4:
a1 <> a2
; ( a1 <= a2 or a2 <= a1 )
( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A )
by A1, A2, A3, A4, RELAT_2:def 6;
hence
( a1 <= a2 or a2 <= a1 )
by ORDERS_2:def 5; verum