let L be transitive antisymmetric with_infima RelStr ; for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L holds
( ex_inf_of X \/ Y,L & "/\" (X \/ Y),L = ("/\" X,L) "/\" ("/\" Y,L) )
let X, Y be set ; ( ex_inf_of X,L & ex_inf_of Y,L implies ( ex_inf_of X \/ Y,L & "/\" (X \/ Y),L = ("/\" X,L) "/\" ("/\" Y,L) ) )
assume that
A1:
ex_inf_of X,L
and
A2:
ex_inf_of Y,L
; ( ex_inf_of X \/ Y,L & "/\" (X \/ Y),L = ("/\" X,L) "/\" ("/\" Y,L) )
set a = ("/\" X,L) "/\" ("/\" Y,L);
A3:
X \/ Y is_>=_than ("/\" X,L) "/\" ("/\" Y,L)
proof
let x be
Element of
L;
LATTICE3:def 8 ( not x in X \/ Y or ("/\" X,L) "/\" ("/\" Y,L) <= x )
assume A4:
x in X \/ Y
;
("/\" X,L) "/\" ("/\" Y,L) <= x
per cases
( x in X or x in Y )
by A4, XBOOLE_0:def 3;
suppose A5:
x in X
;
("/\" X,L) "/\" ("/\" Y,L) <= x
X is_>=_than "/\" X,
L
by A1, YELLOW_0:31;
then A6:
x >= "/\" X,
L
by A5, LATTICE3:def 8;
"/\" X,
L >= ("/\" X,L) "/\" ("/\" Y,L)
by YELLOW_0:23;
hence
("/\" X,L) "/\" ("/\" Y,L) <= x
by A6, ORDERS_2:26;
verum end; suppose A7:
x in Y
;
("/\" X,L) "/\" ("/\" Y,L) <= x
Y is_>=_than "/\" Y,
L
by A2, YELLOW_0:31;
then A8:
x >= "/\" Y,
L
by A7, LATTICE3:def 8;
"/\" Y,
L >= ("/\" X,L) "/\" ("/\" Y,L)
by YELLOW_0:23;
hence
("/\" X,L) "/\" ("/\" Y,L) <= x
by A8, ORDERS_2:26;
verum end;
end;
for b being Element of L st X \/ Y is_>=_than b holds
("/\" X,L) "/\" ("/\" Y,L) >= b
proof
let b be
Element of
L;
( X \/ Y is_>=_than b implies ("/\" X,L) "/\" ("/\" Y,L) >= b )
assume A9:
X \/ Y is_>=_than b
;
("/\" X,L) "/\" ("/\" Y,L) >= b
Y c= X \/ Y
by XBOOLE_1:7;
then
Y is_>=_than b
by A9, YELLOW_0:9;
then A10:
"/\" Y,
L >= b
by A2, YELLOW_0:31;
X c= X \/ Y
by XBOOLE_1:7;
then
X is_>=_than b
by A9, YELLOW_0:9;
then
"/\" X,
L >= b
by A1, YELLOW_0:31;
hence
("/\" X,L) "/\" ("/\" Y,L) >= b
by A10, YELLOW_0:23;
verum
end;
hence
( ex_inf_of X \/ Y,L & "/\" (X \/ Y),L = ("/\" X,L) "/\" ("/\" Y,L) )
by A3, YELLOW_0:31; verum