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 :: thesis: for b being Element of L st Y is_>=_than b holds
"/\" (X,L) >= b

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