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 :: thesis: for a being Element of L2 st X is_<=_than a holds
a >= c
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; :: thesis: verum
end;
ex_sup_of X,L2 by A1, A2, Th14;
hence "\/" (X,L1) = "\/" (X,L2) by A3, A4, Def9; :: thesis: verum