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

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;

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