let M be Matrix of 3,F_Real; lines M = {(Line (M,1)),(Line (M,2)),(Line (M,3))}
A1:
lines M c= {(Line (M,1)),(Line (M,2)),(Line (M,3))}
proof
let x be
object ;
TARSKI:def 3 ( not x in lines M or x in {(Line (M,1)),(Line (M,2)),(Line (M,3))} )
assume
x in lines M
;
x in {(Line (M,1)),(Line (M,2)),(Line (M,3))}
then consider i being
Nat such that A2:
i in Seg 3
and A3:
x = Line (
M,
i)
by MATRIX13:103;
(
i = 1 or
i = 2 or
i = 3 )
by A2, FINSEQ_3:1, ENUMSET1:def 1;
hence
x in {(Line (M,1)),(Line (M,2)),(Line (M,3))}
by A3, ENUMSET1:def 1;
verum
end;
{(Line (M,1)),(Line (M,2)),(Line (M,3))} c= lines M
proof
let x be
object ;
TARSKI:def 3 ( not x in {(Line (M,1)),(Line (M,2)),(Line (M,3))} or x in lines M )
assume
x in {(Line (M,1)),(Line (M,2)),(Line (M,3))}
;
x in lines M
then A4:
(
x = Line (
M,1) or
x = Line (
M,2) or
x = Line (
M,3) )
by ENUMSET1:def 1;
( 1
in Seg 3 & 2
in Seg 3 & 3
in Seg 3 )
by FINSEQ_1:1;
hence
x in lines M
by A4, MATRIX13:103;
verum
end;
hence
lines M = {(Line (M,1)),(Line (M,2)),(Line (M,3))}
by A1; verum