let A be non empty RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum