let POS be OrtAfSp; :: thesis: for M, N being Subset of POS
for M', N' being Subset of (Af POS) st M = M' & N = N' holds
( M // N iff M' // N' )
let M, N be Subset of POS; :: thesis: for M', N' being Subset of (Af POS) st M = M' & N = N' holds
( M // N iff M' // N' )
let M', N' be Subset of (Af POS); :: thesis: ( M = M' & N = N' implies ( M // N iff M' // N' ) )
assume A1:
( M = M' & N = N' )
; :: thesis: ( M // N iff M' // N' )
hereby :: thesis: ( M' // N' implies M // N )
assume
M // N
;
:: thesis: M' // N'then consider a,
b,
c,
d being
Element of
POS such that A2:
(
a <> b &
c <> d )
and A3:
(
M = Line a,
b &
N = Line c,
d )
and A4:
a,
b // c,
d
by Def16;
reconsider a' =
a,
b' =
b,
c' =
c,
d' =
d as
Element of
(Af POS) ;
A5:
a',
b' // c',
d'
by A4, Th48;
(
M' = Line a',
b' &
N' = Line c',
d' )
by A1, A3, Th56;
hence
M' // N'
by A2, A5, AFF_1:51;
:: thesis: verum
end;
assume
M' // N'
; :: thesis: M // N
then consider a', b', c', d' being Element of (Af POS) such that
A6:
( a' <> b' & c' <> d' )
and
A7:
a',b' // c',d'
and
A8:
( M' = Line a',b' & N' = Line c',d' )
by AFF_1:51;
reconsider a = a', b = b', c = c', d = d' as Element of POS ;
A9:
a,b // c,d
by A7, Th48;
( M = Line a,b & N = Line c,d )
by A1, A8, Th56;
hence
M // N
by A6, A9, Def16; :: thesis: verum