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 st ex_sup_of X,L1 holds
"\/" X,L1 = "\/" 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 st ex_sup_of X,L1 holds
"\/" X,L1 = "\/" X,L2
let X be set ; :: thesis: ( ex_sup_of X,L1 implies "\/" X,L1 = "\/" X,L2 )
reconsider c = "\/" X,L1 as Element of L2 by A1;
assume A2: ex_sup_of X,L1 ; :: thesis: "\/" X,L1 = "\/" X,L2
then X is_<=_than "\/" X,L1 by Def9;
then A3: X is_<=_than c by A1, Th2;

A4: now

let a be Element of L2; :: thesis: ( X is_<=_than a implies a >= c )
reconsider b = a as Element of L1 by A1;
assume X is_<=_than a ; :: thesis: a >= c
then X is_<=_than b by A1, Th2;
then b >= "\/" X,L1 by A2, Def9;
hence a >= c by A1, Th1; :: thesis: verum

end;

ex_sup_of X,L2 by A1, A2, Th14;
hence "\/" X,L1 = "\/" X,L2 by A3, A4, Def9; :: thesis: verum