let L be non empty RelStr ; :: thesis: for X, Y being set st ex_inf_of X,L & ( for x being Element of L holds
( x is_<=_than X iff x is_<=_than Y ) ) holds
"/\" X,L = "/\" Y,L
let X, Y be set ; :: thesis: ( ex_inf_of X,L & ( for x being Element of L holds
( x is_<=_than X iff x is_<=_than Y ) ) implies "/\" X,L = "/\" Y,L )
assume A1: ex_inf_of X,L ; :: thesis: ( ex x being Element of L st
( ( x is_<=_than X implies x is_<=_than Y ) implies ( x is_<=_than Y & not x is_<=_than X ) ) or "/\" X,L = "/\" Y,L )
assume A2: for x being Element of L holds
( x is_<=_than X iff x is_<=_than Y ) ; :: thesis: "/\" X,L = "/\" Y,L

A3: now

let b be Element of L; :: thesis: ( Y is_>=_than b implies "/\" X,L >= b )
assume Y is_>=_than b ; :: thesis: "/\" X,L >= b
then X is_>=_than b by A2;
hence "/\" X,L >= b by A1, Def10; :: thesis: verum

end;

X is_>=_than "/\" X,L by A1, Def10;
then A4: Y is_>=_than "/\" X,L by A2;
ex_inf_of Y,L by A1, A2, Th48;
hence "/\" X,L = "/\" Y,L by A4, A3, Def10; :: thesis: verum