:: by Wojciech A. Trybulec and Grzegorz Bancerek

::

:: Received September 19, 1989

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

attr c_{1} is strict ;

struct RelStr -> 1-sorted ;

aggr RelStr(# carrier, InternalRel #) -> RelStr ;

sel InternalRel c_{1} -> Relation of the carrier of c_{1};

end;
struct RelStr -> 1-sorted ;

aggr RelStr(# carrier, InternalRel #) -> RelStr ;

sel InternalRel c

registration
end;

definition

let A be RelStr ;

end;
attr A is reflexive means :Def2: :: ORDERS_2:def 2

the InternalRel of A is_reflexive_in the carrier of A;

the InternalRel of A is_reflexive_in the carrier of A;

attr A is transitive means :Def3: :: ORDERS_2:def 3

the InternalRel of A is_transitive_in the carrier of A;

the InternalRel of A is_transitive_in the carrier of A;

attr A is antisymmetric means :Def4: :: ORDERS_2:def 4

the InternalRel of A is_antisymmetric_in the carrier of A;

the InternalRel of A is_antisymmetric_in the carrier of A;

:: deftheorem Def1 defines total ORDERS_2:def 1 :

for A being RelStr holds

( A is total iff the InternalRel of A is total );

for A being RelStr holds

( A is total iff the InternalRel of A is total );

:: deftheorem Def2 defines reflexive ORDERS_2:def 2 :

for A being RelStr holds

( A is reflexive iff the InternalRel of A is_reflexive_in the carrier of A );

for A being RelStr holds

( A is reflexive iff the InternalRel of A is_reflexive_in the carrier of A );

:: deftheorem Def3 defines transitive ORDERS_2:def 3 :

for A being RelStr holds

( A is transitive iff the InternalRel of A is_transitive_in the carrier of A );

for A being RelStr holds

( A is transitive iff the InternalRel of A is_transitive_in the carrier of A );

:: deftheorem Def4 defines antisymmetric ORDERS_2:def 4 :

for A being RelStr holds

( A is antisymmetric iff the InternalRel of A is_antisymmetric_in the carrier of A );

for A being RelStr holds

( A is antisymmetric iff the InternalRel of A is_antisymmetric_in the carrier of A );

registration

existence

ex b_{1} being RelStr st

( b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is strict & b_{1} is total & b_{1} is 1 -element )

end;
ex b

( b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let X be set ;

let O be reflexive total Relation of X;

coherence

RelStr(# X,O #) is reflexive

end;
let O be reflexive total Relation of X;

coherence

RelStr(# X,O #) is reflexive

proof end;

registration

let X be set ;

let O be transitive total Relation of X;

coherence

RelStr(# X,O #) is transitive

end;
let O be transitive total Relation of X;

coherence

RelStr(# X,O #) is transitive

proof end;

registration

let X be set ;

let O be antisymmetric total Relation of X;

coherence

RelStr(# X,O #) is antisymmetric

end;
let O be antisymmetric total Relation of X;

coherence

RelStr(# X,O #) is antisymmetric

proof end;

Lm1: for x being set

for A being non empty Poset

for S being Subset of A st x in S holds

x is Element of A

;

:: deftheorem defines <= ORDERS_2:def 5 :

for A being RelStr

for a1, a2 being Element of A holds

( a1 <= a2 iff [a1,a2] in the InternalRel of A );

for A being RelStr

for a1, a2 being Element of A holds

( a1 <= a2 iff [a1,a2] in the InternalRel of A );

definition

let A be RelStr ;

let a1, a2 be Element of A;

irreflexivity

for a1 being Element of A holds

( not a1 <= a1 or not a1 <> a1 ) ;

end;
let a1, a2 be Element of A;

irreflexivity

for a1 being Element of A holds

( not a1 <= a1 or not a1 <> a1 ) ;

:: deftheorem defines < ORDERS_2:def 6 :

for A being RelStr

for a1, a2 being Element of A holds

( a1 < a2 iff ( a1 <= a2 & a1 <> a2 ) );

for A being RelStr

for a1, a2 being Element of A holds

( a1 < a2 iff ( a1 <= a2 & a1 <> a2 ) );

definition

let A be non empty reflexive RelStr ;

let a1, a2 be Element of A;

:: original: <=

redefine pred a1 <= a2;

reflexivity

for a1 being Element of A holds (A,b_{1},b_{1})
by Th1;

end;
let a1, a2 be Element of A;

:: original: <=

redefine pred a1 <= a2;

reflexivity

for a1 being Element of A holds (A,b

theorem Th3: :: ORDERS_2:3

for A being transitive RelStr

for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds

a1 <= a3

for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds

a1 <= a3

proof end;

theorem Th5: :: ORDERS_2:5

for A being transitive antisymmetric RelStr

for a1, a2, a3 being Element of A st a1 < a2 & a2 < a3 holds

a1 < a3 by Th3, Th4;

for a1, a2, a3 being Element of A st a1 < a2 & a2 < a3 holds

a1 < a3 by Th3, Th4;

definition

let A be RelStr ;

let IT be Subset of A;

end;
let IT be Subset of A;

attr IT is strongly_connected means :Def7: :: ORDERS_2:def 7

the InternalRel of A is_strongly_connected_in IT;

the InternalRel of A is_strongly_connected_in IT;

:: deftheorem Def7 defines strongly_connected ORDERS_2:def 7 :

for A being RelStr

for IT being Subset of A holds

( IT is strongly_connected iff the InternalRel of A is_strongly_connected_in IT );

for A being RelStr

for IT being Subset of A holds

( IT is strongly_connected iff the InternalRel of A is_strongly_connected_in IT );

registration

let A be RelStr ;

coherence

for b_{1} being Subset of A st b_{1} is empty holds

b_{1} is strongly_connected

end;
coherence

for b

b

proof end;

registration
end;

theorem Th9: :: ORDERS_2:9

for A being non empty reflexive RelStr

for a1, a2 being Element of A holds

( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )

for a1, a2 being Element of A holds

( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )

proof end;

theorem Th11: :: ORDERS_2:11

for A being reflexive RelStr

for a1, a2 being Element of A holds

( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st

( a1 in C & a2 in C ) )

for a1, a2 being Element of A holds

( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st

( a1 in C & a2 in C ) )

proof end;

theorem Th13: :: ORDERS_2:13

for A being RelStr

for T being Subset of A st the InternalRel of A well_orders T holds

T is Chain of A by ORDERS_1:7, Def7;

for T being Subset of A st the InternalRel of A well_orders T holds

T is Chain of A by ORDERS_1:7, Def7;

::

:: Upper and lower cones.

::

:: Upper and lower cones.

::

definition

let A be non empty Poset;

let S be Subset of A;

{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a2 < a1 } is Subset of A

end;
let S be Subset of A;

func UpperCone S -> Subset of A equals :: ORDERS_2:def 8

{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a2 < a1 } ;

coherence { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a2 < a1 } ;

{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a2 < a1 } is Subset of A

proof end;

:: deftheorem defines UpperCone ORDERS_2:def 8 :

for A being non empty Poset

for S being Subset of A holds UpperCone S = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a2 < a1 } ;

for A being non empty Poset

for S being Subset of A holds UpperCone S = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a2 < a1 } ;

definition

let A be non empty Poset;

let S be Subset of A;

{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a1 < a2 } is Subset of A

end;
let S be Subset of A;

func LowerCone S -> Subset of A equals :: ORDERS_2:def 9

{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a1 < a2 } ;

coherence { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a1 < a2 } ;

{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a1 < a2 } is Subset of A

proof end;

:: deftheorem defines LowerCone ORDERS_2:def 9 :

for A being non empty Poset

for S being Subset of A holds LowerCone S = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a1 < a2 } ;

for A being non empty Poset

for S being Subset of A holds LowerCone S = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds

a1 < a2 } ;

theorem Th18: :: ORDERS_2:18

for A being non empty Poset

for a being Element of A

for S being Subset of A st a in S holds

not a in UpperCone S

for a being Element of A

for S being Subset of A st a in S holds

not a in UpperCone S

proof end;

theorem Th20: :: ORDERS_2:20

for A being non empty Poset

for a being Element of A

for S being Subset of A st a in S holds

not a in LowerCone S

for a being Element of A

for S being Subset of A st a in S holds

not a in LowerCone S

proof end;

::

:: Initial segments.

::

:: Initial segments.

::

definition

let A be non empty Poset;

let S be Subset of A;

let a be Element of A;

correctness

coherence

(LowerCone {a}) /\ S is Subset of A;

;

end;
let S be Subset of A;

let a be Element of A;

correctness

coherence

(LowerCone {a}) /\ S is Subset of A;

;

:: deftheorem defines InitSegm ORDERS_2:def 10 :

for A being non empty Poset

for S being Subset of A

for a being Element of A holds InitSegm (S,a) = (LowerCone {a}) /\ S;

for A being non empty Poset

for S being Subset of A

for a being Element of A holds InitSegm (S,a) = (LowerCone {a}) /\ S;

definition

let A be non empty Poset;

let S be Subset of A;

( ( S <> {} implies ex b_{1} being Subset of A ex a being Element of A st

( a in S & b_{1} = InitSegm (S,a) ) ) & ( not S <> {} implies ex b_{1} being Subset of A st b_{1} = {} ) )

for b_{1} being Subset of A holds verum
;

end;
let S be Subset of A;

mode Initial_Segm of S -> Subset of A means :Def11: :: ORDERS_2:def 11

ex a being Element of A st

( a in S & it = InitSegm (S,a) ) if S <> {}

otherwise it = {} ;

existence ex a being Element of A st

( a in S & it = InitSegm (S,a) ) if S <> {}

otherwise it = {} ;

( ( S <> {} implies ex b

( a in S & b

proof end;

consistency for b

:: deftheorem Def11 defines Initial_Segm ORDERS_2:def 11 :

for A being non empty Poset

for S, b_{3} being Subset of A holds

( ( S <> {} implies ( b_{3} is Initial_Segm of S iff ex a being Element of A st

( a in S & b_{3} = InitSegm (S,a) ) ) ) & ( not S <> {} implies ( b_{3} is Initial_Segm of S iff b_{3} = {} ) ) );

for A being non empty Poset

for S, b

( ( S <> {} implies ( b

( a in S & b

theorem Th24: :: ORDERS_2:24

for A being non empty Poset

for a, b being Element of A

for S being Subset of A holds

( a in InitSegm (S,b) iff ( a < b & a in S ) )

for a, b being Element of A

for S being Subset of A holds

( a in InitSegm (S,b) iff ( a < b & a in S ) )

proof end;

theorem :: ORDERS_2:25

theorem Th26: :: ORDERS_2:26

for A being non empty Poset

for a being Element of A

for S being Subset of A holds not a in InitSegm (S,a)

for a being Element of A

for S being Subset of A holds not a in InitSegm (S,a)

proof end;

theorem :: ORDERS_2:27

for A being non empty Poset

for a1, a2 being Element of A

for S being Subset of A st a1 < a2 holds

InitSegm (S,a1) c= InitSegm (S,a2)

for a1, a2 being Element of A

for S being Subset of A st a1 < a2 holds

InitSegm (S,a1) c= InitSegm (S,a2)

proof end;

theorem Th28: :: ORDERS_2:28

for A being non empty Poset

for a being Element of A

for S, T being Subset of A st S c= T holds

InitSegm (S,a) c= InitSegm (T,a)

for a being Element of A

for S, T being Subset of A st S c= T holds

InitSegm (S,a) c= InitSegm (T,a)

proof end;

theorem Th30: :: ORDERS_2:30

for A being non empty Poset

for S being Subset of A holds

( S <> {} iff not S is Initial_Segm of S )

for S being Subset of A holds

( S <> {} iff not S is Initial_Segm of S )

proof end;

theorem Th31: :: ORDERS_2:31

for A being non empty Poset

for S, T being Subset of A st S <> {} & S is Initial_Segm of T holds

not T is Initial_Segm of S

for S, T being Subset of A st S <> {} & S is Initial_Segm of T holds

not T is Initial_Segm of S

proof end;

theorem Th32: :: ORDERS_2:32

for A being non empty Poset

for a1, a2 being Element of A

for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds

a1 in T

for a1, a2 being Element of A

for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds

a1 in T

proof end;

theorem Th33: :: ORDERS_2:33

for A being non empty Poset

for a being Element of A

for S, T being Subset of A st a in S & S is Initial_Segm of T holds

InitSegm (S,a) = InitSegm (T,a)

for a being Element of A

for S, T being Subset of A st a in S & S is Initial_Segm of T holds

InitSegm (S,a) = InitSegm (T,a)

proof end;

theorem :: ORDERS_2:34

for A being non empty Poset

for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds

a1 in S ) & not S = T holds

S is Initial_Segm of T

for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds

a1 in S ) & not S = T holds

S is Initial_Segm of T

proof end;

theorem Th35: :: ORDERS_2:35

for A being non empty Poset

for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds

a1 in S ) & not S = T holds

S is Initial_Segm of T

for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds

a1 in S ) & not S = T holds

S is Initial_Segm of T

proof end;

definition

let A be non empty Poset;

let f be Choice_Function of (BOOL the carrier of A);

ex b_{1} being Chain of A st

( b_{1} <> {} & the InternalRel of A well_orders b_{1} & ( for a being Element of A st a in b_{1} holds

f . (UpperCone (InitSegm (b_{1},a))) = a ) )

end;
let f be Choice_Function of (BOOL the carrier of A);

mode Chain of f -> Chain of A means :Def12: :: ORDERS_2:def 12

( it <> {} & the InternalRel of A well_orders it & ( for a being Element of A st a in it holds

f . (UpperCone (InitSegm (it,a))) = a ) );

existence ( it <> {} & the InternalRel of A well_orders it & ( for a being Element of A st a in it holds

f . (UpperCone (InitSegm (it,a))) = a ) );

ex b

( b

f . (UpperCone (InitSegm (b

proof end;

:: deftheorem Def12 defines Chain ORDERS_2:def 12 :

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A)

for b_{3} being Chain of A holds

( b_{3} is Chain of f iff ( b_{3} <> {} & the InternalRel of A well_orders b_{3} & ( for a being Element of A st a in b_{3} holds

f . (UpperCone (InitSegm (b_{3},a))) = a ) ) );

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A)

for b

( b

f . (UpperCone (InitSegm (b

theorem Th36: :: ORDERS_2:36

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A) holds {(f . the carrier of A)} is Chain of f

for f being Choice_Function of (BOOL the carrier of A) holds {(f . the carrier of A)} is Chain of f

proof end;

theorem Th37: :: ORDERS_2:37

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A)

for fC being Chain of f holds f . the carrier of A in fC

for f being Choice_Function of (BOOL the carrier of A)

for fC being Chain of f holds f . the carrier of A in fC

proof end;

theorem Th38: :: ORDERS_2:38

for A being non empty Poset

for a, b being Element of A

for f being Choice_Function of (BOOL the carrier of A)

for fC being Chain of f st a in fC & b = f . the carrier of A holds

b <= a

for a, b being Element of A

for f being Choice_Function of (BOOL the carrier of A)

for fC being Chain of f st a in fC & b = f . the carrier of A holds

b <= a

proof end;

theorem :: ORDERS_2:39

for A being non empty Poset

for a being Element of A

for f being Choice_Function of (BOOL the carrier of A)

for fC being Chain of f st a = f . the carrier of A holds

InitSegm (fC,a) = {}

for a being Element of A

for f being Choice_Function of (BOOL the carrier of A)

for fC being Chain of f st a = f . the carrier of A holds

InitSegm (fC,a) = {}

proof end;

theorem :: ORDERS_2:40

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A)

for fC1, fC2 being Chain of f holds fC1 meets fC2

for f being Choice_Function of (BOOL the carrier of A)

for fC1, fC2 being Chain of f holds fC1 meets fC2

proof end;

theorem Th41: :: ORDERS_2:41

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A)

for fC1, fC2 being Chain of f st fC1 <> fC2 holds

( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )

for f being Choice_Function of (BOOL the carrier of A)

for fC1, fC2 being Chain of f st fC1 <> fC2 holds

( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )

proof end;

theorem Th42: :: ORDERS_2:42

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A)

for fC1, fC2 being Chain of f holds

( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )

for f being Choice_Function of (BOOL the carrier of A)

for fC1, fC2 being Chain of f holds

( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )

proof end;

definition

let A be non empty Poset;

let f be Choice_Function of (BOOL the carrier of A);

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is Chain of f )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is Chain of f ) ) & ( for x being set holds

( x in b_{2} iff x is Chain of f ) ) holds

b_{1} = b_{2}

end;
let f be Choice_Function of (BOOL the carrier of A);

func Chains f -> set means :Def13: :: ORDERS_2:def 13

for x being set holds

( x in it iff x is Chain of f );

existence for x being set holds

( x in it iff x is Chain of f );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def13 defines Chains ORDERS_2:def 13 :

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A)

for b_{3} being set holds

( b_{3} = Chains f iff for x being set holds

( x in b_{3} iff x is Chain of f ) );

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A)

for b

( b

( x in b

registration

let A be non empty Poset;

let f be Choice_Function of (BOOL the carrier of A);

coherence

not Chains f is empty

end;
let f be Choice_Function of (BOOL the carrier of A);

coherence

not Chains f is empty

proof end;

Lm2: for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) is Subset of A

proof end;

Lm3: for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) is Chain of A

proof end;

theorem Th43: :: ORDERS_2:43

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) <> {}

for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) <> {}

proof end;

theorem Th44: :: ORDERS_2:44

for A being non empty Poset

for S being Subset of A

for f being Choice_Function of (BOOL the carrier of A)

for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds

fC is Initial_Segm of S

for S being Subset of A

for f being Choice_Function of (BOOL the carrier of A)

for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds

fC is Initial_Segm of S

proof end;

theorem Th45: :: ORDERS_2:45

for A being non empty Poset

for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) is Chain of f

for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) is Chain of f

proof end;

::

:: Orders.

::

:: Orders.

::

theorem :: ORDERS_2:47

for A being non empty Poset

for S being Subset of A st the InternalRel of A |_2 S is being_linear-order holds

S is Chain of A

for S being Subset of A st the InternalRel of A |_2 S is being_linear-order holds

S is Chain of A

proof end;

theorem :: ORDERS_2:48

for A being non empty Poset

for C being Chain of A holds the InternalRel of A |_2 C is being_linear-order

for C being Chain of A holds the InternalRel of A |_2 C is being_linear-order

proof end;

theorem :: ORDERS_2:49

for A being non empty Poset

for S being Subset of A st the InternalRel of A linearly_orders S holds

S is Chain of A by ORDERS_1:7, Def7;

for S being Subset of A st the InternalRel of A linearly_orders S holds

S is Chain of A by ORDERS_1:7, Def7;

theorem :: ORDERS_2:51

for A being non empty Poset

for a being Element of A holds

( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )

for a being Element of A holds

( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )

proof end;

theorem :: ORDERS_2:52

for A being non empty Poset

for a being Element of A holds

( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )

for a being Element of A holds

( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )

proof end;

theorem :: ORDERS_2:53

for A being non empty Poset

for a being Element of A holds

( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds

b < a )

for a being Element of A holds

( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds

b < a )

proof end;

theorem :: ORDERS_2:54

for A being non empty Poset

for a being Element of A holds

( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds

a < b )

for a being Element of A holds

( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds

a < b )

proof end;

Lm4: for X, Y being set

for R being Relation st R well_orders X & Y c= X holds

R well_orders Y

proof end;

::

:: Kuratowski - Zorn Lemma.

::

:: Kuratowski - Zorn Lemma.

::

theorem Th55: :: ORDERS_2:55

for A being non empty Poset st ( for C being Chain of A ex a being Element of A st

for b being Element of A st b in C holds

b <= a ) holds

ex a being Element of A st

for b being Element of A holds not a < b

for b being Element of A st b in C holds

b <= a ) holds

ex a being Element of A st

for b being Element of A holds not a < b

proof end;

theorem :: ORDERS_2:56

for A being non empty Poset st ( for C being Chain of A ex a being Element of A st

for b being Element of A st b in C holds

a <= b ) holds

ex a being Element of A st

for b being Element of A holds not b < a

for b being Element of A st b in C holds

a <= b ) holds

ex a being Element of A st

for b being Element of A holds not b < a

proof end;

:: from YELLOW14, 2009.07.26, A.T.

registration
end;

:: Chains.

::