:: Subspaces of Real Linear Space Generated by One, Two, or Three Vectorsand Their Cosets
:: by Wojciech A. Trybulec
::
:: Received February 24, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem :: RLVECT_4:1
theorem :: RLVECT_4:2
canceled;
theorem :: RLVECT_4:3
canceled;
theorem :: RLVECT_4:4
theorem :: RLVECT_4:5
canceled;
theorem Th6: :: RLVECT_4:6
theorem :: RLVECT_4:7
theorem :: RLVECT_4:8
theorem Th9: :: RLVECT_4:9
theorem Th10: :: RLVECT_4:10
theorem Th11: :: RLVECT_4:11
theorem :: RLVECT_4:12
theorem :: RLVECT_4:13
theorem Th14: :: RLVECT_4:14
theorem :: RLVECT_4:15
theorem :: RLVECT_4:16
theorem Th17: :: RLVECT_4:17
theorem :: RLVECT_4:18
theorem :: RLVECT_4:19
theorem :: RLVECT_4:20
theorem :: RLVECT_4:21
theorem Th22: :: RLVECT_4:22
theorem :: RLVECT_4:23
theorem Th24: :: RLVECT_4:24
theorem :: RLVECT_4:25
theorem :: RLVECT_4:26
theorem :: RLVECT_4:27
theorem :: RLVECT_4:28
theorem :: RLVECT_4:29
theorem Th30: :: RLVECT_4:30
theorem Th31: :: RLVECT_4:31
theorem :: RLVECT_4:32
theorem :: RLVECT_4:33
theorem Th34: :: RLVECT_4:34
theorem :: RLVECT_4:35
theorem :: RLVECT_4:36
theorem :: RLVECT_4:37
theorem :: RLVECT_4:38
theorem :: RLVECT_4:39