let A be non empty reflexive RelStr ; for a1, a2 being Element of A holds
( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
let a1, a2 be Element of A; ( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
A1:
a2 <= a2
;
thus
( not {a1,a2} is Chain of A or a1 <= a2 or a2 <= a1 )
( ( a1 <= a2 or a2 <= a1 ) implies {a1,a2} is Chain of A )
assume A3:
( a1 <= a2 or a2 <= a1 )
; {a1,a2} is Chain of A
A4:
a1 <= a1
;
{a1,a2} is strongly_connected
proof
let x,
y be
object ;
RELAT_2:def 7,
ORDERS_2:def 7 ( not x in {a1,a2} or not y in {a1,a2} or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A5:
(
x in {a1,a2} &
y in {a1,a2} )
;
( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence
(
[x,y] in the
InternalRel of
A or
[y,x] in the
InternalRel of
A )
;
verum
end;
hence
{a1,a2} is Chain of A
; verum