let X be set ; :: thesis: for n being Nat
for K being non void subset-closed SimplicialComplexStr
for S being Simplex of n,K st n <= degree K holds
( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
let n be Nat; :: thesis: for K being non void subset-closed SimplicialComplexStr
for S being Simplex of n,K st n <= degree K holds
( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
let K be non void subset-closed SimplicialComplexStr; :: thesis: for S being Simplex of n,K st n <= degree K holds
( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
let S be Simplex of n,K; :: thesis: ( n <= degree K implies ( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) ) )
assume A1: n <= degree K ; :: thesis: ( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
n - 1 <= n - 0 by XREAL_1:6;
then A2: n - 1 <= degree K by A1, XXREAL_0:2;
reconsider N = n as Integer ;
A3: n - 1 >= 0 - 1 by XREAL_1:6;
then A4: max ((n - 1),(- 1)) = n - 1 by XXREAL_0:def 10;
A5: card S = N + 1 by A1, Def18;

hereby :: thesis: ( ex x being set st
( x in S & S \ {x} = X ) implies X is Face of S )

assume X is Face of S ; :: thesis: ex x being set st
( x in S & S \ {x} = X )
then reconsider f = X as Face of S ;
A6: f c= S by A1, Def19;
card f = (n - 1) + 1 by A2, A3, A4, Def18;
then card (S \ f) = (n + 1) - n by A5, A6, CARD_2:44
.= 1 ;
then consider x being object such that
A7: S \ f = {x} by CARD_2:42;
reconsider x = x as set by TARSKI:1;
take x = x; :: thesis: ( x in S & S \ {x} = X )
x in {x} by TARSKI:def 1;
hence x in S by A7, XBOOLE_0:def 5; :: thesis: S \ {x} = X
thus S \ {x} = f /\ S by A7, XBOOLE_1:48
.= X by A6, XBOOLE_1:28 ; :: thesis: verum

end;

given x being set such that A8: x in S and
A9: S \ {x} = X ; :: thesis: X is Face of S
reconsider f = X as finite Simplex of K by A9;
card f = (n - 1) + 1 by A5, A8, A9, STIRL2_1:55;
then A10: f is Simplex of n - 1,K by A2, A3, Def18;
X c= S by A9, XBOOLE_1:36;
hence X is Face of S by A1, A4, A10, Def19; :: thesis: verum