A1:
X includes_lattice_of X
by Def8;

A2: InclPoset X is distributive

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; :: thesis: verum

A2: InclPoset X is distributive

proof

( ( for x, y being set st x in X & y in X holds
let x, y, z be Element of (InclPoset X); :: according to WAYBEL_1:def 3 :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum