let A be non empty reflexive RelStr ; :: thesis: 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; :: thesis: ( {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 ) :: thesis: ( ( a1 <= a2 or a2 <= a1 ) implies {a1,a2} is Chain of A )
proof
assume {a1,a2} is Chain of A ; :: thesis: ( a1 <= a2 or a2 <= a1 )
then A2: the InternalRel of A is_strongly_connected_in {a1,a2} by Def7;
( a1 in {a1,a2} & a2 in {a1,a2} ) by TARSKI:def 2;
then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by A2;
hence ( a1 <= a2 or a2 <= a1 ) ; :: thesis: verum
end;
assume A3: ( a1 <= a2 or a2 <= a1 ) ; :: thesis: {a1,a2} is Chain of A
A4: a1 <= a1 ;
{a1,a2} is strongly_connected
proof
let x, y be object ; :: according to RELAT_2:def 7,ORDERS_2:def 7 :: thesis: ( 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} ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
now :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
per cases ( ( x = a1 & y = a1 ) or ( x = a1 & y = a2 ) or ( x = a2 & y = a1 ) or ( x = a2 & y = a2 ) ) by A5, TARSKI:def 2;
suppose ( x = a1 & y = a1 ) ; :: thesis: ( [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 ) by A4; :: thesis: verum
end;
suppose ( x = a1 & y = a2 ) ; :: thesis: ( [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 ) by A3; :: thesis: verum
end;
suppose ( x = a2 & y = a1 ) ; :: thesis: ( [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 ) by A3; :: thesis: verum
end;
suppose ( x = a2 & y = a2 ) ; :: thesis: ( [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 ) by A1; :: thesis: verum
end;
end;
end;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: thesis: verum
end;
hence {a1,a2} is Chain of A ; :: thesis: verum