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: a _|_ b ; :: thesis: ( not a _|_ c or ( a _|_ b "/\" c & a _|_ b "\/" c ) )
assume b: a _|_ c ; :: thesis: ( a _|_ b "/\" c & a _|_ b "\/" c )
c: a [= b ` by orthogonal, a;
d: a [= c ` by orthogonal, b;
b ` [= (b ` ) "\/" (c ` ) by LATTICES:22;
then a [= (b ` ) "\/" (c ` ) by c, LATTICES:25;
then a [= (((b ` ) "\/" (c ` )) ` ) ` by ROBBINS3:def 6;
then a [= (b "/\" c) ` by ROBBINS1:def 23;
hence a _|_ b "/\" c by orthogonal; :: thesis: a _|_ b "\/" c
a "/\" (c ` ) [= (b ` ) "/\" (c ` ) by c, LATTICES:27;
then a [= (b ` ) "/\" (c ` ) by d, LATTICES:21;
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 by orthogonal; :: thesis: verum