:: On Cosets in Segre's Product of Partial Linear Spaces
:: by Adam Naumowicz
::
:: Received August 14, 2001
:: Copyright (c) 2001 Association of Mizar Users
:: deftheorem defines Del PENCIL_2:def 1 :
theorem Th1: :: PENCIL_2:1
theorem Th2: :: PENCIL_2:2
theorem Th3: :: PENCIL_2:3
theorem Th4: :: PENCIL_2:4
theorem Th5: :: PENCIL_2:5
theorem Th6: :: PENCIL_2:6
theorem Th7: :: PENCIL_2:7
:: deftheorem Def2 defines Segre-Coset PENCIL_2:def 2 :
theorem Th8: :: PENCIL_2:8
:: deftheorem Def3 defines are_joinable PENCIL_2:def 3 :
theorem :: PENCIL_2:9
theorem Th10: :: PENCIL_2:10
theorem Th11: :: PENCIL_2:11
theorem :: PENCIL_2:12
:: deftheorem Def4 defines isomorphic PENCIL_2:def 4 :
theorem Th13: :: PENCIL_2:13
theorem Th14: :: PENCIL_2:14
theorem :: PENCIL_2:15
theorem Th16: :: PENCIL_2:16
theorem :: PENCIL_2:17
theorem Th18: :: PENCIL_2:18
theorem :: PENCIL_2:19
theorem Th20: :: PENCIL_2:20
theorem :: PENCIL_2:21
theorem Th22: :: PENCIL_2:22
theorem Th23: :: PENCIL_2:23
theorem Th24: :: PENCIL_2:24
theorem :: PENCIL_2:25