let L be non empty reflexive transitive RelStr ; :: thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow R,C,c,L ) holds
SupBelow R,C is strict_chain of R
let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow R,C,c,L ) holds
SupBelow R,C is strict_chain of R
let C be strict_chain of R; :: thesis: ( ( for c being Element of L holds ex_sup_of SetBelow R,C,c,L ) implies SupBelow R,C is strict_chain of R )
assume A1: for c being Element of L holds ex_sup_of SetBelow R,C,c,L ; :: thesis: SupBelow R,C is strict_chain of R
thus SupBelow R,C is strict_chain of R :: thesis: verum

proof

let a, b be set ; :: according to WAYBEL35:def 3 :: thesis: ( a in SupBelow R,C & b in SupBelow R,C & not [a,b] in R & not a = b implies [b,a] in R )
assume A2: a in SupBelow R,C ; :: thesis: ( not b in SupBelow R,C or [a,b] in R or a = b or [b,a] in R )
then A3: a = sup (SetBelow R,C,a) by Def10;
reconsider a = a as Element of L by A2;
A4: a <= a ;
A5: ex_sup_of SetBelow R,C,a,L by A1;
assume A6: b in SupBelow R,C ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )
then A7: b = sup (SetBelow R,C,b) by Def10;
reconsider b = b as Element of L by A6;
A8: b <= b ;
A9: ex_sup_of SetBelow R,C,b,L by A1;

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) ; :: thesis: verum

end;

suppose A10: a <> b ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

( ( for x being Element of L st x in C holds
( [x,a] in R iff [x,b] in R ) ) implies a = b )

proof

assume A11: for x being Element of L st x in C holds
( [x,a] in R iff [x,b] in R ) ; :: thesis: a = b
SetBelow R,C,a = SetBelow R,C,b

proof

thus SetBelow R,C,a c= SetBelow R,C,b :: according to XBOOLE_0:def 10 :: thesis: SetBelow R,C,b c= SetBelow R,C,a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SetBelow R,C,a or x in SetBelow R,C,b )
assume A12: x in SetBelow R,C,a ; :: thesis: x in SetBelow R,C,b
then reconsider x = x as Element of L ;
A13: x in C by A12, Th18;
[x,a] in R by A12, Th18;
then [x,b] in R by A13, A11;
hence x in SetBelow R,C,b by A13, Th18; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SetBelow R,C,b or x in SetBelow R,C,a )
assume A14: x in SetBelow R,C,b ; :: thesis: x in SetBelow R,C,a
then reconsider x = x as Element of L ;
A15: x in C by A14, Th18;
[x,b] in R by A14, Th18;
then [x,a] in R by A15, A11;
hence x in SetBelow R,C,a by A15, Th18; :: thesis: verum

end;

hence a = b by A2, A7, Def10; :: thesis: verum

end;

then consider x being Element of L such that
A16: x in C and
A17: ( ( [x,a] in R & not [x,b] in R ) or ( not [x,a] in R & [x,b] in R ) ) by A10;
A18: x <= x ;
thus ( [a,b] in R or a = b or [b,a] in R ) :: thesis: verum

proof

per cases ( ( [x,a] in R & not [x,b] in R ) or ( not [x,a] in R & [x,b] in R ) ) by A17;

suppose that A19: [x,a] in R and
A20: not [x,b] in R ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

SetBelow R,C,b is_<=_than x

proof

let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in SetBelow R,C,b or y <= x )
assume A21: y in SetBelow R,C,b ; :: thesis: y <= x
then [y,b] in R by Th18;
then A22: y <= b by WAYBEL_4:def 4;
y in C by A21, Th18;
then ( [y,x] in R or x = y or [x,y] in R ) by A16, Def3;
hence y <= x by A18, A20, A22, WAYBEL_4:def 4, WAYBEL_4:def 5; :: thesis: verum

end;

then b <= x by A7, A9, YELLOW_0:def 9;
hence ( [a,b] in R or a = b or [b,a] in R ) by A4, A19, WAYBEL_4:def 5; :: thesis: verum

end;

suppose that A23: not [x,a] in R and
A24: [x,b] in R ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

SetBelow R,C,a is_<=_than x

proof

let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in SetBelow R,C,a or y <= x )
assume A25: y in SetBelow R,C,a ; :: thesis: y <= x
then [y,a] in R by Th18;
then A26: y <= a by WAYBEL_4:def 4;
y in C by A25, Th18;
then ( [y,x] in R or x = y or [x,y] in R ) by A16, Def3;
hence y <= x by A18, A23, A26, WAYBEL_4:def 4, WAYBEL_4:def 5; :: thesis: verum

end;

then a <= x by A3, A5, YELLOW_0:def 9;
hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A24, WAYBEL_4:def 5; :: thesis: verum

end;

end;

end;

end;

end;

end;