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 a' = a as Element of L2 by A1;
take a' ; :: according to YELLOW_0:def 7 :: thesis: ( X is_<=_than a' & ( for b being Element of L2 st X is_<=_than b holds
b >= a' ) & ( 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 = a' ) )
thus X is_<=_than a' by A1, A2, Th2; :: thesis: ( ( for b being Element of L2 st X is_<=_than b holds
b >= a' ) & ( 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 = a' ) )

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 = a'

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

end;

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

now

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

end;

hence c' = a' 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 a' = a as Element of L2 by A1;
take a' ; :: according to YELLOW_0:def 8 :: thesis: ( X is_>=_than a' & ( for b being Element of L2 st X is_>=_than b holds
b <= a' ) & ( 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 = a' ) )
thus X is_>=_than a' by A1, A7, Th2; :: thesis: ( ( for b being Element of L2 st X is_>=_than b holds
b <= a' ) & ( 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 = a' ) )

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 = a'

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

end;

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

now

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

end;

hence c' = a' by A9, A10; :: thesis: verum