:: deftheorem Def7 defines face TRIANG_1:def 7 :
for T being lower_non-empty TriangStr
for n being Nat
for x being Symplex of T,(n + 1)
for f being Face of n st the SkeletonSeq of T . (n + 1) <> {} holds
for b₅ being Symplex of T,n holds
( b₅ = face (x,f) iff for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b₅ = G . x );