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 )
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 ;
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 ; :: thesis: verum
end;
assume A3: X = { v where v is Element of V : L . v <> 0 } ; :: thesis:
thus X c= Carrier :: according to XBOOLE_0:def 10 :: thesis:
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Carrier )
assume x in X ; :: thesis:
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