A1:
X includes_lattice_of X
by Def8;
A2:
InclPoset X is distributive
proof
let x,
y,
z be
Element of
(InclPoset X);
WAYBEL_1:def 3 x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
x in the
carrier of
(InclPoset X)
;
then A3:
x in X
by YELLOW_1:1;
z in the
carrier of
(InclPoset X)
;
then A4:
z in X
by YELLOW_1:1;
then A5:
x /\ z in X
by A1, A3;
then A6:
x "/\" z = x /\ z
by YELLOW_1:9;
y in the
carrier of
(InclPoset X)
;
then A7:
y in X
by YELLOW_1:1;
then A8:
y \/ z in X
by A1, A4;
then reconsider r =
y \/ z as
Element of
(InclPoset X) by YELLOW_1:1;
A9:
x /\ y in X
by A1, A3, A7;
then reconsider r1 =
x /\ y,
r2 =
x /\ z as
Element of
(InclPoset X) by A5, YELLOW_1:1;
r1 in the
carrier of
(InclPoset X)
;
then A10:
r1 in 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, A3;
then
x "/\" r = x /\ r
by YELLOW_1:9;
then A11:
(
x /\ (y \/ z) = (x /\ y) \/ (x /\ z) &
x /\ (y \/ z) = x "/\" (y "\/" z) )
by A8, XBOOLE_1:23, YELLOW_1:8;
r2 in the
carrier of
(InclPoset X)
;
then
r2 in X
by YELLOW_1:1;
then A12:
r1 \/ r2 in X
by A1, A10;
x "/\" y = x /\ y
by A9, YELLOW_1:9;
hence
x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
by A11, A6, A12, YELLOW_1:8;
verum
end;
( ( for x, y being set st x in X & y in X holds
x /\ y in X ) & ( for x, y being set st x in X & y in X holds
x \/ y in X ) )
by A1;
hence
( InclPoset X is with_suprema & InclPoset X is with_infima & InclPoset X is distributive )
by A2, YELLOW_1:11, YELLOW_1:12; verum