let L be non empty transitive RelStr ; :: thesis: for S being non empty full SubRelStr of L
for X being Subset of S st ex_sup_of X,L & "\/" (X,L) in the carrier of S holds
( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )
let S be non empty full SubRelStr of L; :: thesis: for X being Subset of S st ex_sup_of X,L & "\/" (X,L) in the carrier of S holds
( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )
let X be Subset of S; :: thesis: ( ex_sup_of X,L & "\/" (X,L) in the carrier of S implies ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) )
assume that
A1: ex_sup_of X,L and
A2: "\/" (X,L) in the carrier of S ; :: thesis: ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )
reconsider a = "\/" (X,L) as Element of S by A2;
A3: now :: thesis: ( a is_>=_than X & ( for b being Element of S st b is_>=_than X holds
b >= a ) )
"\/" (X,L) is_>=_than X by A1, Def9;
hence a is_>=_than X by Th61; :: thesis: for b being Element of S st b is_>=_than X holds
b >= a
let b be Element of S; :: thesis: ( b is_>=_than X implies b >= a )
reconsider b9 = b as Element of L by Th58;
assume b is_>=_than X ; :: thesis: b >= a
then b9 is_>=_than X by Th62;
then b9 >= "\/" (X,L) by A1, Def9;
hence b >= a by Th60; :: thesis: verum
end;
consider a9 being Element of L such that
A4: X is_<=_than a9 and
A5: for b being Element of L st X is_<=_than b holds
b >= a9 and
for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
b >= c ) holds
c = a9 by A1;
A6: a9 = "\/" (X,L) by A1, A4, A5, Def9;
thus ex_sup_of X,S :: thesis: "\/" (X,S) = "\/" (X,L)
proof
take a ; :: according to YELLOW_0:def 7 :: thesis: ( X is_<=_than a & ( for b being Element of S st X is_<=_than b holds
b >= a ) & ( for c being Element of S st X is_<=_than c & ( for b being Element of S st X is_<=_than b holds
b >= c ) holds
c = a ) )
thus ( a is_>=_than X & ( for b being Element of S st b is_>=_than X holds
b >= a ) ) by A3; :: thesis: for c being Element of S st X is_<=_than c & ( for b being Element of S st X is_<=_than b holds
b >= c ) holds
c = a
let c be Element of S; :: thesis: ( X is_<=_than c & ( for b being Element of S st X is_<=_than b holds
b >= c ) implies c = a )
reconsider c9 = c as Element of L by Th58;
assume X is_<=_than c ; :: thesis: ( ex b being Element of S st
( X is_<=_than b & not b >= c ) or c = a )
then A7: X is_<=_than c9 by Th62;
assume for b being Element of S st X is_<=_than b holds
b >= c ; :: thesis: c = a
then A8: a >= c by A3;
now :: thesis: for b being Element of L st X is_<=_than b holds
b >= c9
let b be Element of L; :: thesis: ( X is_<=_than b implies b >= c9 )
assume X is_<=_than b ; :: thesis: b >= c9
then A9: b >= a9 by A5;
a9 >= c9 by A6, A8, Th59;
hence b >= c9 by A9, ORDERS_2:3; :: thesis: verum
end;
hence c = a by A1, A7, Def9; :: thesis: verum
end;
hence "\/" (X,S) = "\/" (X,L) by A3, Def9; :: thesis: verum