let L be distributive lower-bounded pseudocomplemented Lattice; :: thesis: for a, b being Element of L st a in Skeleton L & b in Skeleton L holds
a "/\" b in Skeleton L
let a, b be Element of L; :: thesis: ( a in Skeleton L & b in Skeleton L implies a "/\" b in Skeleton L )
assume ( a in Skeleton L & b in Skeleton L ) ; :: thesis: a "/\" b in Skeleton L
then A2: ( a = (a *) * & b = (b *) * ) by Th13;
a * [= (a "/\" b) * by Th6, LATTICES:6;
then B2: ((a "/\" b) *) * [= a by A2, Th6;
b * [= (a "/\" b) * by Th6, LATTICES:6;
then ((a "/\" b) *) * [= (b *) * by Th6;
then B1: ((a "/\" b) *) * [= a "/\" b by B2, FILTER_0:7, A2;
a "/\" b [= ((a "/\" b) *) * by Th5;
then a "/\" b = ((a "/\" b) *) * by B1, LATTICES:8;
hence a "/\" b in Skeleton L ; :: thesis: verum