let L1, L2 be RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X being set holds
( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) ) )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for X being set holds
( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) )
let X be set ; :: thesis: ( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) )
thus ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) :: thesis: ( ex_inf_of X,L1 implies ex_inf_of X,L2 )

proof

given a being Element of L1 such that A2: X is_<=_than a and
A3: for b being Element of L1 st X is_<=_than b holds
b >= a and
A4: for c being Element of L1 st X is_<=_than c & ( for b being Element of L1 st X is_<=_than b holds
b >= c ) holds
c = a ; :: according to YELLOW_0:def 7 :: thesis: ex_sup_of X,L2
reconsider a9 = a as Element of L2 by A1;
take a9 ; :: according to YELLOW_0:def 7 :: thesis: ( X is_<=_than a9 & ( for b being Element of L2 st X is_<=_than b holds
b >= a9 ) & ( for c being Element of L2 st X is_<=_than c & ( for b being Element of L2 st X is_<=_than b holds
b >= c ) holds
c = a9 ) )
thus X is_<=_than a9 by A1, A2, Th2; :: thesis: ( ( for b being Element of L2 st X is_<=_than b holds
b >= a9 ) & ( for c being Element of L2 st X is_<=_than c & ( for b being Element of L2 st X is_<=_than b holds
b >= c ) holds
c = a9 ) )

hereby :: thesis: for c being Element of L2 st X is_<=_than c & ( for b being Element of L2 st X is_<=_than b holds
b >= c ) holds
c = a9

let b9 be Element of L2; :: thesis: ( X is_<=_than b9 implies b9 >= a9 )
reconsider b = b9 as Element of L1 by A1;
assume X is_<=_than b9 ; :: thesis: b9 >= a9
then b >= a by A1, A3, Th2;
hence b9 >= a9 by A1; :: thesis: verum

end;

let c9 be Element of L2; :: thesis: ( X is_<=_than c9 & ( for b being Element of L2 st X is_<=_than b holds
b >= c9 ) implies c9 = a9 )
reconsider c = c9 as Element of L1 by A1;
assume X is_<=_than c9 ; :: thesis: ( ex b being Element of L2 st
( X is_<=_than b & not b >= c9 ) or c9 = a9 )
then A5: X is_<=_than c by A1, Th2;
assume A6: for b9 being Element of L2 st X is_<=_than b9 holds
b9 >= c9 ; :: thesis: c9 = a9

now :: thesis: for b being Element of L1 st X is_<=_than b holds
b >= c

let b be Element of L1; :: thesis: ( X is_<=_than b implies b >= c )
reconsider b9 = b as Element of L2 by A1;
assume X is_<=_than b ; :: thesis: b >= c
then b9 >= c9 by A1, A6, Th2;
hence b >= c by A1; :: thesis: verum

end;

hence c9 = a9 by A4, A5; :: thesis: verum

end;

given a being Element of L1 such that A7: X is_>=_than a and
A8: for b being Element of L1 st X is_>=_than b holds
b <= a and
A9: for c being Element of L1 st X is_>=_than c & ( for b being Element of L1 st X is_>=_than b holds
b <= c ) holds
c = a ; :: according to YELLOW_0:def 8 :: thesis: ex_inf_of X,L2
reconsider a9 = a as Element of L2 by A1;
take a9 ; :: according to YELLOW_0:def 8 :: thesis: ( X is_>=_than a9 & ( for b being Element of L2 st X is_>=_than b holds
b <= a9 ) & ( for c being Element of L2 st X is_>=_than c & ( for b being Element of L2 st X is_>=_than b holds
b <= c ) holds
c = a9 ) )
thus X is_>=_than a9 by A1, A7, Th2; :: thesis: ( ( for b being Element of L2 st X is_>=_than b holds
b <= a9 ) & ( for c being Element of L2 st X is_>=_than c & ( for b being Element of L2 st X is_>=_than b holds
b <= c ) holds
c = a9 ) )

hereby :: thesis: for c being Element of L2 st X is_>=_than c & ( for b being Element of L2 st X is_>=_than b holds
b <= c ) holds
c = a9

let b9 be Element of L2; :: thesis: ( X is_>=_than b9 implies b9 <= a9 )
reconsider b = b9 as Element of L1 by A1;
assume X is_>=_than b9 ; :: thesis: b9 <= a9
then b <= a by A1, A8, Th2;
hence b9 <= a9 by A1; :: thesis: verum

end;

let c9 be Element of L2; :: thesis: ( X is_>=_than c9 & ( for b being Element of L2 st X is_>=_than b holds
b <= c9 ) implies c9 = a9 )
reconsider c = c9 as Element of L1 by A1;
assume A10: X is_>=_than c9 ; :: thesis: ( ex b being Element of L2 st
( X is_>=_than b & not b <= c9 ) or c9 = a9 )
assume A11: for b9 being Element of L2 st X is_>=_than b9 holds
b9 <= c9 ; :: thesis: c9 = a9

A12: now :: thesis: for b being Element of L1 st X is_>=_than b holds
b <= c

let b be Element of L1; :: thesis: ( X is_>=_than b implies b <= c )
reconsider b9 = b as Element of L2 by A1;
assume X is_>=_than b ; :: thesis: b <= c
then b9 <= c9 by A1, A11, Th2;
hence b <= c by A1; :: thesis: verum

end;

X is_>=_than c by A1, A10, Th2;
hence c9 = a9 by A9, A12; :: thesis: verum