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