let X be Subset of V; :: thesis: ( X = Carrier iff X = { v where v is Element of V : L . v <> 0 } )

set A = Carrier ;

set B = { v where v is Element of V : L . v <> 0 } ;

thus ( X = Carrier implies X = { v where v is Element of V : L . v <> 0 } ) :: thesis: ( X = { v where v is Element of V : L . v <> 0 } implies X = Carrier )

thus X c= Carrier :: according to XBOOLE_0:def 10 :: thesis: Carrier c= X

assume A4: x in Carrier ; :: thesis: x in X

then A5: L . x <> 0 by PRE_POLY:def 7;

Carrier c= the carrier of V by Lm1;

hence x in X by A3, A4, A5; :: thesis: verum

set A = Carrier ;

set B = { v where v is Element of V : L . v <> 0 } ;

thus ( X = Carrier implies X = { v where v is Element of V : L . v <> 0 } ) :: thesis: ( X = { v where v is Element of V : L . v <> 0 } implies X = Carrier )

proof

assume A3:
X = { v where v is Element of V : L . v <> 0 }
; :: thesis: X = Carrier
assume A1:
X = Carrier
; :: thesis: X = { v where v is Element of V : L . v <> 0 }

thus X c= { v where v is Element of V : L . v <> 0 } :: according to XBOOLE_0:def 10 :: thesis: { v where v is Element of V : L . v <> 0 } c= X

assume x in { v where v is Element of V : L . v <> 0 } ; :: thesis: x in X

then ex v being Element of V st

( x = v & L . v <> 0 ) ;

hence x in X by A1, PRE_POLY:def 7; :: thesis: verum

end;thus X c= { v where v is Element of V : L . v <> 0 } :: according to XBOOLE_0:def 10 :: thesis: { v where v is Element of V : L . v <> 0 } c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of V : L . v <> 0 } or x in X )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in { v where v is Element of V : L . v <> 0 } )

assume A2: x in X ; :: thesis: x in { v where v is Element of V : L . v <> 0 }

then L . x <> 0 by A1, PRE_POLY:def 7;

hence x in { v where v is Element of V : L . v <> 0 } by A2; :: thesis: verum

end;assume A2: x in X ; :: thesis: x in { v where v is Element of V : L . v <> 0 }

then L . x <> 0 by A1, PRE_POLY:def 7;

hence x in { v where v is Element of V : L . v <> 0 } by A2; :: thesis: verum

assume x in { v where v is Element of V : L . v <> 0 } ; :: thesis: x in X

then ex v being Element of V st

( x = v & L . v <> 0 ) ;

hence x in X by A1, PRE_POLY:def 7; :: thesis: verum

thus X c= Carrier :: according to XBOOLE_0:def 10 :: thesis: Carrier c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier or x in X )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Carrier )

assume x in X ; :: thesis: x in Carrier

then ex v being Element of V st

( x = v & L . v <> 0 ) by A3;

hence x in Carrier by PRE_POLY:def 7; :: thesis: verum

end;assume x in X ; :: thesis: x in Carrier

then ex v being Element of V st

( x = v & L . v <> 0 ) by A3;

hence x in Carrier by PRE_POLY:def 7; :: thesis: verum

assume A4: x in Carrier ; :: thesis: x in X

then A5: L . x <> 0 by PRE_POLY:def 7;

Carrier c= the carrier of V by Lm1;

hence x in X by A3, A4, A5; :: thesis: verum