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 that
A1:
M = M'
and
A2:
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 A3:
(
a <> b &
c <> d &
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:
M' = Line a',
b'
by A1, A3, Th56;
A6:
N' = Line c',
d'
by A2, A3, Th56;
a',
b' // c',
d'
by A4, Th48;
hence
M' // N'
by A3, A5, A6, 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
A7:
( a' <> b' & c' <> d' )
and
A8:
a',b' // c',d'
and
A9:
( 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 ;
A10:
M = Line a,b
by A1, A9, Th56;
A11:
N = Line c,d
by A2, A9, Th56;
a,b // c,d
by A8, Th48;
hence
M // N
by A7, A10, A11, Def16; :: thesis: verum