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

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:
reconsider a9 = a as Element of L2 by A1;
take a9 ; :: according to YELLOW_0:def 7 :: thesis:
thus X is_<=_than a9 by A1, A2, Th2; :: thesis:

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

end;

let c9 be Element of L2; :: thesis:
reconsider c = c9 as Element of L1 by A1;
assume X is_<=_than c9 ; :: thesis:
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:

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

end;

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

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:
reconsider a9 = a as Element of L2 by A1;
take a9 ; :: according to YELLOW_0:def 8 :: thesis:
thus X is_>=_than a9 by A1, A7, Th2; :: thesis:

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

end;

let c9 be Element of L2; :: thesis:
reconsider c = c9 as Element of L1 by A1;
assume A10: X is_>=_than c9 ; :: thesis:
assume A11: for b9 being Element of L2 st X is_>=_than b9 holds
b9 <= c9 ; :: thesis:

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

end;