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;
assume A4: b in SupBelow R,C ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )
then A5: b = sup (SetBelow R,C,b) by Def10;
reconsider b = b as Element of L by A4;
A6: a <= a ;
A7: b <= b ;
A8: ex_sup_of SetBelow R,C,a,L by A1;
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 ;
( [x,a] in R & x in C ) by A12, Th18;
then ( [x,b] in R & x in C ) by A11;
hence x in SetBelow R,C,b by 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 A13: x in SetBelow R,C,b ; :: thesis: x in SetBelow R,C,a
then reconsider x = x as Element of L ;
( [x,b] in R & x in C ) by A13, Th18;
then ( [x,a] in R & x in C ) by A11;
hence x in SetBelow R,C,a by Th18; :: thesis: verum

end;

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

end;

then consider x being Element of L such that
A14: x in C and
A15: ( ( [x,a] in R & not [x,b] in R ) or ( not [x,a] in R & [x,b] in R ) ) by A10;
A16: 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 A15;

suppose that A17: [x,a] in R and
A18: 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 A19: y in SetBelow R,C,b ; :: thesis: y <= x
then [y,b] in R by Th18;
then A20: y <= b by WAYBEL_4:def 4;
y in C by A19, Th18;
then ( [y,x] in R or x = y or [x,y] in R ) by A14, Def3;
hence y <= x by A16, A18, A20, WAYBEL_4:def 4, WAYBEL_4:def 5; :: thesis: verum

end;

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

end;

suppose that A21: not [x,a] in R and
A22: [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 A23: y in SetBelow R,C,a ; :: thesis: y <= x
then [y,a] in R by Th18;
then A24: y <= a by WAYBEL_4:def 4;
y in C by A23, Th18;
then ( [y,x] in R or x = y or [x,y] in R ) by A14, Def3;
hence y <= x by A16, A21, A24, WAYBEL_4:def 4, WAYBEL_4:def 5; :: thesis: verum

end;

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

end;

end;

end;

end;

end;

end;