let L be transitive antisymmetric with_infima RelStr ; :: thesis: 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 ; :: thesis: ( 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
; :: thesis: ( 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;
:: according to LATTICE3:def 8 :: thesis: ( not x in X \/ Y or ("/\" X,L) "/\" ("/\" Y,L) <= x )
assume A4:
x in X \/ Y
;
:: thesis: ("/\" 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
;
:: thesis: ("/\" X,L) "/\" ("/\" Y,L) <= x
X is_>=_than "/\" X,
L
by A1, YELLOW_0:31;
then
(
x >= "/\" X,
L &
"/\" X,
L >= ("/\" X,L) "/\" ("/\" Y,L) )
by A5, LATTICE3:def 8, YELLOW_0:23;
hence
x >= ("/\" X,L) "/\" ("/\" Y,L)
by ORDERS_2:26;
:: thesis: verum end; suppose A6:
x in Y
;
:: thesis: ("/\" X,L) "/\" ("/\" Y,L) <= x
Y is_>=_than "/\" Y,
L
by A2, YELLOW_0:31;
then
(
x >= "/\" Y,
L &
"/\" Y,
L >= ("/\" X,L) "/\" ("/\" Y,L) )
by A6, LATTICE3:def 8, YELLOW_0:23;
hence
x >= ("/\" X,L) "/\" ("/\" Y,L)
by ORDERS_2:26;
:: thesis: 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;
:: thesis: ( X \/ Y is_>=_than b implies ("/\" X,L) "/\" ("/\" Y,L) >= b )
assume A7:
X \/ Y is_>=_than b
;
:: thesis: ("/\" X,L) "/\" ("/\" Y,L) >= b
(
X c= X \/ Y &
Y c= X \/ Y )
by XBOOLE_1:7;
then
(
X is_>=_than b &
Y is_>=_than b )
by A7, YELLOW_0:9;
then
(
"/\" X,
L >= b &
"/\" Y,
L >= b )
by A1, A2, YELLOW_0:31;
hence
("/\" X,L) "/\" ("/\" Y,L) >= b
by YELLOW_0:23;
:: thesis: verum
end;
hence
( ex_inf_of X \/ Y,L & "/\" (X \/ Y),L = ("/\" X,L) "/\" ("/\" Y,L) )
by A3, YELLOW_0:31; :: thesis: verum