let POS be OrtAfSp; for a, b, c, d, p, q being Element of POS st p <> q & ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) holds
a,b _|_ c,d
let a, b, c, d, p, q be Element of POS; ( p <> q & ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) implies a,b _|_ c,d )
assume that
A1:
p <> q
and
A2:
( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) )
; a,b _|_ c,d
A3:
now ( ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // a,b & c,d _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) ) implies a,b _|_ c,d )assume
( (
p,
q // a,
b &
p,
q _|_ c,
d ) or (
p,
q // a,
b &
c,
d _|_ p,
q ) or (
a,
b // p,
q &
c,
d _|_ p,
q ) or (
a,
b // p,
q &
p,
q _|_ c,
d ) )
;
a,b _|_ c,dthen
(
p,
q // a,
b &
p,
q _|_ c,
d )
by Th59, Th61;
then
c,
d _|_ a,
b
by A1, Def7;
hence
a,
b _|_ c,
d
by Th61;
verum end;
now ( ( ( p,q // c,d & p,q _|_ a,b ) or ( p,q // c,d & a,b _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( c,d // p,q & p,q _|_ a,b ) ) implies a,b _|_ c,d )assume
( (
p,
q // c,
d &
p,
q _|_ a,
b ) or (
p,
q // c,
d &
a,
b _|_ p,
q ) or (
c,
d // p,
q &
a,
b _|_ p,
q ) or (
c,
d // p,
q &
p,
q _|_ a,
b ) )
;
a,b _|_ c,dthen
(
p,
q // c,
d &
p,
q _|_ a,
b )
by Th59, Th61;
hence
a,
b _|_ c,
d
by A1, Def7;
verum end;
hence
a,b _|_ c,d
by A2, A3; verum