A1: X includes_lattice_of X by Def8;
A2: InclPoset X is distributive
proof
let x, y, z be Element of (); :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
x in the carrier of () ;
then A3: x in X by YELLOW_1:1;
z in the carrier of () ;
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 () ;
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 () by YELLOW_1:1;
A9: x /\ y in X by A1, A3, A7;
then reconsider r1 = x /\ y, r2 = x /\ z as Element of () by ;
r1 in the carrier of () ;
then A10: r1 in X by YELLOW_1:1;
r in the carrier of () ;
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 ;
r2 in the carrier of () ;
then r2 in X by YELLOW_1:1;
then A12: r1 \/ r2 in X by ;
x "/\" y = x /\ y by ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by ; :: thesis: 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 ; :: thesis: verum