let POS be non empty ParOrtStr ; for K, M being Subset of POS holds
( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) )
let K, M be Subset of POS; ( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) )
hereby ( ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) implies K _|_ M )
assume
K _|_ M
;
ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d )then consider a,
b being
Element of
POS such that A1:
(
a <> b &
K = Line (
a,
b) )
and A2:
a,
b _|_ M
;
ex
c,
d being
Element of
POS st
(
c <> d &
M = Line (
c,
d) &
a,
b _|_ c,
d )
by A2;
hence
ex
a,
b,
c,
d being
Element of
POS st
(
a <> b &
c <> d &
K = Line (
a,
b) &
M = Line (
c,
d) &
a,
b _|_ c,
d )
by A1;
verum
end;
given a, b, c, d being Element of POS such that A3:
a <> b
and
A4:
c <> d
and
A5:
K = Line (a,b)
and
A6:
( M = Line (c,d) & a,b _|_ c,d )
; K _|_ M
a,b _|_ M
by A4, A6;
hence
K _|_ M
by A3, A5; verum