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

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, Th1; :: thesis: verum

end;

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