let F be Field; :: thesis: for S being OrtSp of F

for a, b, x being Element of S st not a _|_ holds

a _|_

let S be OrtSp of F; :: thesis: for a, b, x being Element of S st not a _|_ holds

a _|_

let a, b, x be Element of S; :: thesis: ( not a _|_ implies a _|_ )

assume A1: not a _|_ ; :: thesis: a _|_

then ex l being Element of F st a _|_ by Def1;

hence a _|_ by A1, Def2; :: thesis: verum

for a, b, x being Element of S st not a _|_ holds

a _|_

let S be OrtSp of F; :: thesis: for a, b, x being Element of S st not a _|_ holds

a _|_

let a, b, x be Element of S; :: thesis: ( not a _|_ implies a _|_ )

assume A1: not a _|_ ; :: thesis: a _|_

then ex l being Element of F st a _|_ by Def1;

hence a _|_ by A1, Def2; :: thesis: verum