:: deftheorem defines Model PRELAMB:def 16 :
for s being non empty typealg
for A being non empty set
for b₃ being Function of the carrier of s,(bool (A *)) holds
( b₃ is Model of s,A iff for x, y being type of s holds
( b₃ . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in b₃ . x & b in b₃ . y ) } & b₃ . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in b₃ . y holds
a1 ^ b in b₃ . x } & b₃ . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in b₃ . y holds
b ^ a2 in b₃ . x } ) );