let L1, L2 be RelStr ; ( 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 #)
; for X being set st ex_inf_of X,L1 holds
"/\" (X,L1) = "/\" (X,L2)
let X be set ; ( 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
; "/\" (X,L1) = "/\" (X,L2)
then
X is_>=_than "/\" (X,L1)
by Def10;
then A3:
X is_>=_than c
by A1, Th2;
ex_inf_of X,L2
by A1, A2, Th14;
hence
"/\" (X,L1) = "/\" (X,L2)
by A3, A4, Def10; verum