let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds
( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX )
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX holds
( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX )
let SX be SubSimplicialComplex of KX; :: thesis: ( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX )

hereby :: thesis: ( (bool ([#] SX)) /\ the topology of KX c= the topology of SX implies SX is maximal )

assume A1: SX is maximal ; :: thesis: (bool ([#] SX)) /\ the topology of KX c= the topology of SX
thus (bool ([#] SX)) /\ the topology of KX c= the topology of SX :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (bool ([#] SX)) /\ the topology of KX or x in the topology of SX )
assume A2: x in (bool ([#] SX)) /\ the topology of KX ; :: thesis: x in the topology of SX
then reconsider A = x as Subset of SX by XBOOLE_0:def 4;
A in the topology of KX by A2, XBOOLE_0:def 4;
then A is simplex-like by A1;
hence x in the topology of SX ; :: thesis: verum

end;

end;

assume A3: (bool ([#] SX)) /\ the topology of KX c= the topology of SX ; :: thesis: SX is maximal
let A be Subset of SX; :: according to SIMPLEX0:def 14 :: thesis: ( A in the topology of KX implies A is simplex-like )
assume A in the topology of KX ; :: thesis: A is simplex-like
then A in (bool ([#] SX)) /\ the topology of KX by XBOOLE_0:def 4;
hence A is simplex-like by A3; :: thesis: verum