A1:
X includes_lattice_of X
by Def8;
A2:
InclPoset X is LATTICE
InclPoset X is distributive
proof
let x,
y,
z be
Element of
(InclPoset X);
:: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A4:
x /\ (y \/ z) = (x /\ y) \/ (x /\ z)
by XBOOLE_1:23;
x in the
carrier of
(InclPoset X)
;
then A5:
x in X
by YELLOW_1:1;
y in the
carrier of
(InclPoset X)
;
then A6:
y in X
by YELLOW_1:1;
z in the
carrier of
(InclPoset X)
;
then A7:
z in X
by YELLOW_1:1;
then A8:
y \/ z in X
by A1, A6, COHSP_1:def 8;
then reconsider r =
y \/ z as
Element of
(InclPoset X) by YELLOW_1:1;
r in the
carrier of
(InclPoset X)
;
then
r in X
by YELLOW_1:1;
then
x /\ r in X
by A1, A5, COHSP_1:def 8;
then
x "/\" r = x /\ r
by YELLOW_1:9;
then A9:
x /\ (y \/ z) = x "/\" (y "\/" z)
by A8, YELLOW_1:8;
A10:
x /\ y in X
by A1, A5, A6, COHSP_1:def 8;
then A11:
x "/\" y = x /\ y
by YELLOW_1:9;
A12:
x /\ z in X
by A1, A5, A7, COHSP_1:def 8;
then reconsider r1 =
x /\ y,
r2 =
x /\ z as
Element of
(InclPoset X) by A10, YELLOW_1:1;
A13:
x "/\" z = x /\ z
by A12, YELLOW_1:9;
r2 in the
carrier of
(InclPoset X)
;
then A14:
r2 in X
by YELLOW_1:1;
r1 in the
carrier of
(InclPoset X)
;
then
r1 in X
by YELLOW_1:1;
then
r1 \/ r2 in X
by A1, A14, COHSP_1:def 8;
hence
x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
by A4, A9, A11, A13, YELLOW_1:8;
:: thesis: verum
end;
hence
( InclPoset X is with_suprema & InclPoset X is with_infima & InclPoset X is distributive )
by A2; :: thesis: verum