let X be Subset of V; :: thesis: ( X = Carrier iff X = { v where v is Element of V : L . v <> 0c } )
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 <> 0c } implies X = Carrier )

proof

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

proof

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;

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 )
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;

assume A3: X = { v where v is Element of V : L . v <> 0 } ; :: thesis: X = Carrier
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 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;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier or x in 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