let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for A being Subset of V holds
( Int A = A iff A is trivial )
let A be Subset of V; :: thesis: ( Int A = A iff A is trivial )
per cases ( A is empty or not A is empty ) ;
suppose A is empty ; :: thesis: ( Int A = A iff A is trivial )
hence ( Int A = A iff A is trivial ) ; :: thesis: verum
end;
suppose A1: not A is empty ; :: thesis: ( Int A = A iff A is trivial )
hereby :: thesis: ( A is trivial implies Int A = A )
assume A2: Int A = A ; :: thesis: A is trivial
now :: thesis: for x, y being object st x in A & y in A holds
x = y
let x, y be object ; :: thesis: ( x in A & y in A implies x = y )
assume that
A3: x in A and
A4: y in A ; :: thesis: x = y
( A \ {x} c= A & A \ {x} <> A ) by A3, ZFMISC_1:56;
then ( A \ {x} c= conv (A \ {x}) & A \ {x} c< A ) by RLAFFIN1:2;
then not y in A \ {x} by A2, Def1;
hence x = y by A4, ZFMISC_1:56; :: thesis: verum
end;
hence A is trivial by ZFMISC_1:def 10; :: thesis: verum
end;
assume A is trivial ; :: thesis: Int A = A
then consider v being Element of V such that
A5: A = {v} by A1, SUBSET_1:47;
A6: for B being Subset of V holds
( not B c< A or not v in conv B )
proof
let B be Subset of V; :: thesis: ( not B c< A or not v in conv B )
assume A7: B c< A ; :: thesis: not v in conv B
B is empty by A5, A7, ZFMISC_1:33;
hence not v in conv B ; :: thesis: verum
end;
A8: conv A = A by A5, RLAFFIN1:1;
then A9: Int A c= A by Lm2;
v in A by A5, TARSKI:def 1;
then v in Int A by A6, A8, Def1;
hence Int A = A by A5, A9, ZFMISC_1:33; :: thesis: verum
end;
end;