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