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_inf_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_inf_of X,L1 holds
"/\" (X,L1) = "/\" (X,L2)
let X be set ; :: thesis: ( ex_inf_of X,L1 implies "/\" (X,L1) = "/\" (X,L2) )
reconsider c = "/\" (X,L1) as Element of L2 by A1;
assume A2: ex_inf_of X,L1 ; :: thesis: "/\" (X,L1) = "/\" (X,L2)
then X is_>=_than "/\" (X,L1) by Def10;
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, Def10;
hence a <= c by A1; :: thesis: verum

end;

ex_inf_of X,L2 by A1, A2, Th14;
hence "/\" (X,L1) = "/\" (X,L2) by A3, A4, Def10; :: thesis: verum