let L be Ortholattice; :: thesis: for a, b, c being Element of L st a _|_ b & a _|_ c holds

( a _|_ b "/\" c & a _|_ b "\/" c )

let a, b, c be Element of L; :: thesis: ( a _|_ b & a _|_ c implies ( a _|_ b "/\" c & a _|_ b "\/" c ) )

assume a _|_ b ; :: thesis: ( not a _|_ c or ( a _|_ b "/\" c & a _|_ b "\/" c ) )

then A1: a [= b ` ;

then A2: a "/\" (c `) [= (b `) "/\" (c `) by LATTICES:9;

assume A3: a _|_ c ; :: thesis: ( a _|_ b "/\" c & a _|_ b "\/" c )

b ` [= (b `) "\/" (c `) by LATTICES:5;

then a [= (b `) "\/" (c `) by A1, LATTICES:7;

then a [= (((b `) "\/" (c `)) `) ` by ROBBINS3:def 6;

then a [= (b "/\" c) ` by ROBBINS1:def 23;

hence a _|_ b "/\" c ; :: thesis: a _|_ b "\/" c

a [= c ` by A3;

then a [= (b `) "/\" (c `) by A2, LATTICES:4;

then a [= (((b `) `) "\/" ((c `) `)) ` by ROBBINS1:def 23;

then a [= (b "\/" ((c `) `)) ` by ROBBINS3:def 6;

then a [= (b "\/" c) ` by ROBBINS3:def 6;

hence a _|_ b "\/" c ; :: thesis: verum

( a _|_ b "/\" c & a _|_ b "\/" c )

let a, b, c be Element of L; :: thesis: ( a _|_ b & a _|_ c implies ( a _|_ b "/\" c & a _|_ b "\/" c ) )

assume a _|_ b ; :: thesis: ( not a _|_ c or ( a _|_ b "/\" c & a _|_ b "\/" c ) )

then A1: a [= b ` ;

then A2: a "/\" (c `) [= (b `) "/\" (c `) by LATTICES:9;

assume A3: a _|_ c ; :: thesis: ( a _|_ b "/\" c & a _|_ b "\/" c )

b ` [= (b `) "\/" (c `) by LATTICES:5;

then a [= (b `) "\/" (c `) by A1, LATTICES:7;

then a [= (((b `) "\/" (c `)) `) ` by ROBBINS3:def 6;

then a [= (b "/\" c) ` by ROBBINS1:def 23;

hence a _|_ b "/\" c ; :: thesis: a _|_ b "\/" c

a [= c ` by A3;

then a [= (b `) "/\" (c `) by A2, LATTICES:4;

then a [= (((b `) `) "\/" ((c `) `)) ` by ROBBINS1:def 23;

then a [= (b "\/" ((c `) `)) ` by ROBBINS3:def 6;

then a [= (b "\/" c) ` by ROBBINS3:def 6;

hence a _|_ b "\/" c ; :: thesis: verum