set KI = { h where h is Element of EnsHomography3 : h is_K-isometry } ;
{ h where h is Element of EnsHomography3 : h is_K-isometry } c= EnsHomography3
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { h where h is Element of EnsHomography3 : h is_K-isometry } or x in EnsHomography3 )
assume x in { h where h is Element of EnsHomography3 : h is_K-isometry } ; :: thesis: x in EnsHomography3
then ex h being Element of EnsHomography3 st
( x = h & h is_K-isometry ) ;
hence x in EnsHomography3 ; :: thesis: verum
end;
then reconsider KI = { h where h is Element of EnsHomography3 : h is_K-isometry } as Subset of EnsHomography3 ;
reconsider N = 1. (F_Real,3) as invertible Matrix of 3,F_Real ;
homography N in { (homography N) where N is invertible Matrix of 3,F_Real : verum } ;
then reconsider h = homography N as Element of EnsHomography3 by ANPROJ_9:def 1;
h is_K-isometry by Th33;
then h in KI ;
hence { h where h is Element of EnsHomography3 : h is_K-isometry } is non empty Subset of EnsHomography3 ; :: thesis: verum